Step | Hyp | Ref
| Expression |
1 | | dfcnqs 6917 |
. 2
⊢ ℂ =
((R × R) / ◡ E ) |
2 | | addcnsrec 6918 |
. 2
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ([〈𝑧, 𝑤〉]◡ E + [〈𝑣, 𝑢〉]◡ E ) = [〈(𝑧 +R 𝑣), (𝑤 +R 𝑢)〉]◡ E ) |
3 | | mulcnsrec 6919 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ ((𝑧
+R 𝑣) ∈ R ∧ (𝑤 +R
𝑢) ∈ R))
→ ([〈𝑥, 𝑦〉]◡ E · [〈(𝑧 +R 𝑣), (𝑤 +R 𝑢)〉]◡ E ) = [〈((𝑥 ·R (𝑧 +R
𝑣))
+R (-1R
·R (𝑦 ·R (𝑤 +R
𝑢)))), ((𝑦 ·R (𝑧 +R
𝑣))
+R (𝑥 ·R (𝑤 +R
𝑢)))〉]◡ E ) |
4 | | mulcnsrec 6919 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ([〈𝑥, 𝑦〉]◡ E · [〈𝑧, 𝑤〉]◡ E ) = [〈((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))), ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤))〉]◡ E ) |
5 | | mulcnsrec 6919 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ([〈𝑥, 𝑦〉]◡ E · [〈𝑣, 𝑢〉]◡ E ) = [〈((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))), ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢))〉]◡ E ) |
6 | | addcnsrec 6918 |
. 2
⊢
(((((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R ∧ ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R) ∧ (((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R ∧ ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)) ∈ R)) →
([〈((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))), ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤))〉]◡ E + [〈((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))), ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢))〉]◡ E ) = [〈(((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) +R ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢)))), (((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) +R ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)))〉]◡ E ) |
7 | | addclsr 6838 |
. . . 4
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
+R 𝑣) ∈ R) |
8 | | addclsr 6838 |
. . . 4
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
+R 𝑢) ∈ R) |
9 | 7, 8 | anim12i 321 |
. . 3
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
10 | 9 | an4s 522 |
. 2
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
11 | | mulclsr 6839 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑧 ∈ R)
→ (𝑥
·R 𝑧) ∈ R) |
12 | | m1r 6837 |
. . . . . 6
⊢
-1R ∈ R |
13 | | mulclsr 6839 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R)
→ (𝑦
·R 𝑤) ∈ R) |
14 | | mulclsr 6839 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R 𝑤) ∈ R) →
(-1R ·R (𝑦
·R 𝑤)) ∈ R) |
15 | 12, 13, 14 | sylancr 393 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R)
→ (-1R ·R (𝑦
·R 𝑤)) ∈ R) |
16 | | addclsr 6838 |
. . . . 5
⊢ (((𝑥
·R 𝑧) ∈ R ∧
(-1R ·R (𝑦
·R 𝑤)) ∈ R) → ((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
17 | 11, 15, 16 | syl2an 273 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑧 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑤
∈ R)) → ((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
18 | 17 | an4s 522 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
19 | | mulclsr 6839 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ (𝑦
·R 𝑧) ∈ R) |
20 | | mulclsr 6839 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑤 ∈ R)
→ (𝑥
·R 𝑤) ∈ R) |
21 | | addclsr 6838 |
. . . . 5
⊢ (((𝑦
·R 𝑧) ∈ R ∧ (𝑥
·R 𝑤) ∈ R) → ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R) |
22 | 19, 20, 21 | syl2anr 274 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑤 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑧
∈ R)) → ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ∈ R) |
23 | 22 | an42s 523 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ∈ R) |
24 | 18, 23 | jca 290 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R ∧ ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R)) |
25 | | mulclsr 6839 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑣 ∈ R)
→ (𝑥
·R 𝑣) ∈ R) |
26 | | mulclsr 6839 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑢 ∈ R)
→ (𝑦
·R 𝑢) ∈ R) |
27 | | mulclsr 6839 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R 𝑢) ∈ R) →
(-1R ·R (𝑦
·R 𝑢)) ∈ R) |
28 | 12, 26, 27 | sylancr 393 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑢 ∈ R)
→ (-1R ·R (𝑦
·R 𝑢)) ∈ R) |
29 | | addclsr 6838 |
. . . . 5
⊢ (((𝑥
·R 𝑣) ∈ R ∧
(-1R ·R (𝑦
·R 𝑢)) ∈ R) → ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R) |
30 | 25, 28, 29 | syl2an 273 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑣 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑢
∈ R)) → ((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R) |
31 | 30 | an4s 522 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R) |
32 | | mulclsr 6839 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑣 ∈ R)
→ (𝑦
·R 𝑣) ∈ R) |
33 | | mulclsr 6839 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑢 ∈ R)
→ (𝑥
·R 𝑢) ∈ R) |
34 | | addclsr 6838 |
. . . . 5
⊢ (((𝑦
·R 𝑣) ∈ R ∧ (𝑥
·R 𝑢) ∈ R) → ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)) ∈ R) |
35 | 32, 33, 34 | syl2anr 274 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑢 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑣
∈ R)) → ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢)) ∈ R) |
36 | 35 | an42s 523 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢)) ∈ R) |
37 | 31, 36 | jca 290 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R ∧ ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)) ∈ R)) |
38 | | simp1l 928 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑥 ∈
R) |
39 | | simp2l 930 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑧 ∈
R) |
40 | | simp3l 932 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑣 ∈
R) |
41 | | distrsrg 6844 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑧 ∈ R
∧ 𝑣 ∈
R) → (𝑥
·R (𝑧 +R 𝑣)) = ((𝑥 ·R 𝑧) +R
(𝑥
·R 𝑣))) |
42 | 38, 39, 40, 41 | syl3anc 1135 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (𝑧 +R 𝑣)) = ((𝑥 ·R 𝑧) +R
(𝑥
·R 𝑣))) |
43 | | simp1r 929 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑦 ∈
R) |
44 | | simp2r 931 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑤 ∈
R) |
45 | | simp3r 933 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑢 ∈
R) |
46 | | distrsrg 6844 |
. . . . . . 7
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R
∧ 𝑢 ∈
R) → (𝑦
·R (𝑤 +R 𝑢)) = ((𝑦 ·R 𝑤) +R
(𝑦
·R 𝑢))) |
47 | 43, 44, 45, 46 | syl3anc 1135 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R (𝑤 +R 𝑢)) = ((𝑦 ·R 𝑤) +R
(𝑦
·R 𝑢))) |
48 | 47 | oveq2d 5528 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R (𝑤 +R 𝑢))) =
(-1R ·R ((𝑦
·R 𝑤) +R (𝑦
·R 𝑢)))) |
49 | 12 | a1i 9 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
-1R ∈ R) |
50 | 43, 44, 13 | syl2anc 391 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R 𝑤) ∈ R) |
51 | 43, 45, 26 | syl2anc 391 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R 𝑢) ∈ R) |
52 | | distrsrg 6844 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R 𝑤) ∈ R ∧ (𝑦
·R 𝑢) ∈ R) →
(-1R ·R ((𝑦
·R 𝑤) +R (𝑦
·R 𝑢))) = ((-1R
·R (𝑦 ·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢)))) |
53 | 49, 50, 51, 52 | syl3anc 1135 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R ((𝑦
·R 𝑤) +R (𝑦
·R 𝑢))) = ((-1R
·R (𝑦 ·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢)))) |
54 | 48, 53 | eqtrd 2072 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R (𝑤 +R 𝑢))) =
((-1R ·R (𝑦
·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢)))) |
55 | 42, 54 | oveq12d 5530 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑥
·R (𝑧 +R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R
(𝑥
·R 𝑣)) +R
((-1R ·R (𝑦
·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢))))) |
56 | 38, 39, 11 | syl2anc 391 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R 𝑧) ∈ R) |
57 | 38, 40, 25 | syl2anc 391 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R 𝑣) ∈ R) |
58 | 12, 50, 14 | sylancr 393 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R 𝑤)) ∈ R) |
59 | | addcomsrg 6840 |
. . . . 5
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
+R 𝑔) = (𝑔 +R 𝑓)) |
60 | 59 | adantl 262 |
. . . 4
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
+R 𝑔) = (𝑔 +R 𝑓)) |
61 | | addasssrg 6841 |
. . . . 5
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
+R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R
ℎ))) |
62 | 61 | adantl 262 |
. . . 4
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R ∧ ℎ
∈ R)) → ((𝑓 +R 𝑔) +R
ℎ) = (𝑓 +R (𝑔 +R
ℎ))) |
63 | 12, 51, 27 | sylancr 393 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R 𝑢)) ∈ R) |
64 | | addclsr 6838 |
. . . . 5
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
+R 𝑔) ∈ R) |
65 | 64 | adantl 262 |
. . . 4
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
+R 𝑔) ∈ R) |
66 | 56, 57, 58, 60, 62, 63, 65 | caov4d 5685 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑥
·R 𝑧) +R (𝑥
·R 𝑣)) +R
((-1R ·R (𝑦
·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢)))) = (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) +R ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))))) |
67 | 55, 66 | eqtrd 2072 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑥
·R (𝑧 +R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) +R ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))))) |
68 | | distrsrg 6844 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R
∧ 𝑣 ∈
R) → (𝑦
·R (𝑧 +R 𝑣)) = ((𝑦 ·R 𝑧) +R
(𝑦
·R 𝑣))) |
69 | 43, 39, 40, 68 | syl3anc 1135 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R (𝑧 +R 𝑣)) = ((𝑦 ·R 𝑧) +R
(𝑦
·R 𝑣))) |
70 | | distrsrg 6844 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑤 ∈ R
∧ 𝑢 ∈
R) → (𝑥
·R (𝑤 +R 𝑢)) = ((𝑥 ·R 𝑤) +R
(𝑥
·R 𝑢))) |
71 | 38, 44, 45, 70 | syl3anc 1135 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (𝑤 +R 𝑢)) = ((𝑥 ·R 𝑤) +R
(𝑥
·R 𝑢))) |
72 | 69, 71 | oveq12d 5530 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑦
·R (𝑧 +R 𝑣)) +R
(𝑥
·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R
(𝑦
·R 𝑣)) +R ((𝑥
·R 𝑤) +R (𝑥
·R 𝑢)))) |
73 | 43, 39, 19 | syl2anc 391 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R 𝑧) ∈ R) |
74 | 43, 40, 32 | syl2anc 391 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R 𝑣) ∈ R) |
75 | 38, 44, 20 | syl2anc 391 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R 𝑤) ∈ R) |
76 | 38, 45, 33 | syl2anc 391 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R 𝑢) ∈ R) |
77 | 73, 74, 75, 60, 62, 76, 65 | caov4d 5685 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑦
·R 𝑧) +R (𝑦
·R 𝑣)) +R ((𝑥
·R 𝑤) +R (𝑥
·R 𝑢))) = (((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) +R ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)))) |
78 | 72, 77 | eqtrd 2072 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑦
·R (𝑧 +R 𝑣)) +R
(𝑥
·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) +R ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)))) |
79 | 1, 2, 3, 4, 5, 6, 10, 24, 37, 67, 78 | ecovidi 6218 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |