| Step | Hyp | Ref
| Expression |
| 1 | | dfcnqs 11182 |
. 2
⊢ ℂ =
((R × R) / ◡ E ) |
| 2 | | addcnsrec 11183 |
. 2
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ([〈𝑧, 𝑤〉]◡ E + [〈𝑣, 𝑢〉]◡ E ) = [〈(𝑧 +R 𝑣), (𝑤 +R 𝑢)〉]◡ E ) |
| 3 | | mulcnsrec 11184 |
. 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 11184 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ([〈𝑥, 𝑦〉]◡ E · [〈𝑧, 𝑤〉]◡ E ) = [〈((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))), ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤))〉]◡ E ) |
| 5 | | mulcnsrec 11184 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ([〈𝑥, 𝑦〉]◡ E · [〈𝑣, 𝑢〉]◡ E ) = [〈((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))), ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢))〉]◡ E ) |
| 6 | | addcnsrec 11183 |
. 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 11123 |
. . . 4
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
+R 𝑣) ∈ R) |
| 8 | | addclsr 11123 |
. . . 4
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
+R 𝑢) ∈ R) |
| 9 | 7, 8 | anim12i 613 |
. . 3
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
| 10 | 9 | an4s 660 |
. 2
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧
(𝑤
+R 𝑢) ∈ R)) |
| 11 | | mulclsr 11124 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑧 ∈ R)
→ (𝑥
·R 𝑧) ∈ R) |
| 12 | | m1r 11122 |
. . . . . 6
⊢
-1R ∈ R |
| 13 | | mulclsr 11124 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R)
→ (𝑦
·R 𝑤) ∈ R) |
| 14 | | mulclsr 11124 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R 𝑤) ∈ R) →
(-1R ·R (𝑦
·R 𝑤)) ∈ R) |
| 15 | 12, 13, 14 | sylancr 587 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R)
→ (-1R ·R (𝑦
·R 𝑤)) ∈ R) |
| 16 | | addclsr 11123 |
. . . . 5
⊢ (((𝑥
·R 𝑧) ∈ R ∧
(-1R ·R (𝑦
·R 𝑤)) ∈ R) → ((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
| 17 | 11, 15, 16 | syl2an 596 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑧 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑤
∈ R)) → ((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
| 18 | 17 | an4s 660 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
| 19 | | mulclsr 11124 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ (𝑦
·R 𝑧) ∈ R) |
| 20 | | mulclsr 11124 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑤 ∈ R)
→ (𝑥
·R 𝑤) ∈ R) |
| 21 | | addclsr 11123 |
. . . . 5
⊢ (((𝑦
·R 𝑧) ∈ R ∧ (𝑥
·R 𝑤) ∈ R) → ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R) |
| 22 | 19, 20, 21 | syl2anr 597 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑤 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑧
∈ R)) → ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ∈ R) |
| 23 | 22 | an42s 661 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ∈ R) |
| 24 | 18, 23 | jca 511 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R ∧ ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R)) |
| 25 | | mulclsr 11124 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑣 ∈ R)
→ (𝑥
·R 𝑣) ∈ R) |
| 26 | | mulclsr 11124 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑢 ∈ R)
→ (𝑦
·R 𝑢) ∈ R) |
| 27 | | mulclsr 11124 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R 𝑢) ∈ R) →
(-1R ·R (𝑦
·R 𝑢)) ∈ R) |
| 28 | 12, 26, 27 | sylancr 587 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑢 ∈ R)
→ (-1R ·R (𝑦
·R 𝑢)) ∈ R) |
| 29 | | addclsr 11123 |
. . . . 5
⊢ (((𝑥
·R 𝑣) ∈ R ∧
(-1R ·R (𝑦
·R 𝑢)) ∈ R) → ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R) |
| 30 | 25, 28, 29 | syl2an 596 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑣 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑢
∈ R)) → ((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R) |
| 31 | 30 | an4s 660 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R) |
| 32 | | mulclsr 11124 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑣 ∈ R)
→ (𝑦
·R 𝑣) ∈ R) |
| 33 | | mulclsr 11124 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑢 ∈ R)
→ (𝑥
·R 𝑢) ∈ R) |
| 34 | | addclsr 11123 |
. . . . 5
⊢ (((𝑦
·R 𝑣) ∈ R ∧ (𝑥
·R 𝑢) ∈ R) → ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)) ∈ R) |
| 35 | 32, 33, 34 | syl2anr 597 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑢 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑣
∈ R)) → ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢)) ∈ R) |
| 36 | 35 | an42s 661 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑦 ·R 𝑣) +R
(𝑥
·R 𝑢)) ∈ R) |
| 37 | 31, 36 | jca 511 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (((𝑥 ·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢))) ∈ R ∧ ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢)) ∈ R)) |
| 38 | | distrsr 11131 |
. . . 4
⊢ (𝑥
·R (𝑧 +R 𝑣)) = ((𝑥 ·R 𝑧) +R
(𝑥
·R 𝑣)) |
| 39 | | distrsr 11131 |
. . . . . 6
⊢ (𝑦
·R (𝑤 +R 𝑢)) = ((𝑦 ·R 𝑤) +R
(𝑦
·R 𝑢)) |
| 40 | 39 | oveq2i 7442 |
. . . . 5
⊢
(-1R ·R (𝑦
·R (𝑤 +R 𝑢))) =
(-1R ·R ((𝑦
·R 𝑤) +R (𝑦
·R 𝑢))) |
| 41 | | distrsr 11131 |
. . . . 5
⊢
(-1R ·R ((𝑦
·R 𝑤) +R (𝑦
·R 𝑢))) = ((-1R
·R (𝑦 ·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢))) |
| 42 | 40, 41 | eqtri 2765 |
. . . 4
⊢
(-1R ·R (𝑦
·R (𝑤 +R 𝑢))) =
((-1R ·R (𝑦
·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢))) |
| 43 | 38, 42 | oveq12i 7443 |
. . 3
⊢ ((𝑥
·R (𝑧 +R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R
(𝑥
·R 𝑣)) +R
((-1R ·R (𝑦
·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢)))) |
| 44 | | ovex 7464 |
. . . 4
⊢ (𝑥
·R 𝑧) ∈ V |
| 45 | | ovex 7464 |
. . . 4
⊢ (𝑥
·R 𝑣) ∈ V |
| 46 | | ovex 7464 |
. . . 4
⊢
(-1R ·R (𝑦
·R 𝑤)) ∈ V |
| 47 | | addcomsr 11127 |
. . . 4
⊢ (𝑓 +R
𝑔) = (𝑔 +R 𝑓) |
| 48 | | addasssr 11128 |
. . . 4
⊢ ((𝑓 +R
𝑔)
+R ℎ) = (𝑓 +R (𝑔 +R
ℎ)) |
| 49 | | ovex 7464 |
. . . 4
⊢
(-1R ·R (𝑦
·R 𝑢)) ∈ V |
| 50 | 44, 45, 46, 47, 48, 49 | caov4 7664 |
. . 3
⊢ (((𝑥
·R 𝑧) +R (𝑥
·R 𝑣)) +R
((-1R ·R (𝑦
·R 𝑤)) +R
(-1R ·R (𝑦
·R 𝑢)))) = (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) +R ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢)))) |
| 51 | 43, 50 | eqtri 2765 |
. 2
⊢ ((𝑥
·R (𝑧 +R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) +R ((𝑥
·R 𝑣) +R
(-1R ·R (𝑦
·R 𝑢)))) |
| 52 | | distrsr 11131 |
. . . 4
⊢ (𝑦
·R (𝑧 +R 𝑣)) = ((𝑦 ·R 𝑧) +R
(𝑦
·R 𝑣)) |
| 53 | | distrsr 11131 |
. . . 4
⊢ (𝑥
·R (𝑤 +R 𝑢)) = ((𝑥 ·R 𝑤) +R
(𝑥
·R 𝑢)) |
| 54 | 52, 53 | oveq12i 7443 |
. . 3
⊢ ((𝑦
·R (𝑧 +R 𝑣)) +R
(𝑥
·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R
(𝑦
·R 𝑣)) +R ((𝑥
·R 𝑤) +R (𝑥
·R 𝑢))) |
| 55 | | ovex 7464 |
. . . 4
⊢ (𝑦
·R 𝑧) ∈ V |
| 56 | | ovex 7464 |
. . . 4
⊢ (𝑦
·R 𝑣) ∈ V |
| 57 | | ovex 7464 |
. . . 4
⊢ (𝑥
·R 𝑤) ∈ V |
| 58 | | ovex 7464 |
. . . 4
⊢ (𝑥
·R 𝑢) ∈ V |
| 59 | 55, 56, 57, 47, 48, 58 | caov4 7664 |
. . 3
⊢ (((𝑦
·R 𝑧) +R (𝑦
·R 𝑣)) +R ((𝑥
·R 𝑤) +R (𝑥
·R 𝑢))) = (((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) +R ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢))) |
| 60 | 54, 59 | eqtri 2765 |
. 2
⊢ ((𝑦
·R (𝑧 +R 𝑣)) +R
(𝑥
·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) +R ((𝑦
·R 𝑣) +R (𝑥
·R 𝑢))) |
| 61 | 1, 2, 3, 4, 5, 6, 10, 24, 37, 51, 60 | ecovdi 8865 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶))) |