Step | Hyp | Ref
| Expression |
1 | | dfcnqs 7761 |
. 2
⊢ ℂ =
((R × R) / ◡ E ) |
2 | | mulcnsrec 7763 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ([〈𝑥, 𝑦〉]◡ E · [〈𝑧, 𝑤〉]◡ E ) = [〈((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))), ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤))〉]◡ E ) |
3 | | mulcnsrec 7763 |
. 2
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ([〈𝑧, 𝑤〉]◡ E · [〈𝑣, 𝑢〉]◡ E ) = [〈((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))), ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))〉]◡ E ) |
4 | | mulcnsrec 7763 |
. 2
⊢
(((((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R ∧ ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R) ∧ (𝑣 ∈ R ∧
𝑢 ∈ R))
→ ([〈((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))), ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤))〉]◡ E · [〈𝑣, 𝑢〉]◡ E ) = [〈((((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑣) +R
(-1R ·R (((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑢))), ((((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ·R 𝑣) +R
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑢))〉]◡ E ) |
5 | | mulcnsrec 7763 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R ∧ ((𝑤
·R 𝑣) +R (𝑧
·R 𝑢)) ∈ R)) →
([〈𝑥, 𝑦〉]◡ E · [〈((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))), ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))〉]◡ E ) = [〈((𝑥 ·R ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) +R
(-1R ·R (𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))))), ((𝑦 ·R ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) +R (𝑥
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))))〉]◡ E ) |
6 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑧 ∈ R)
→ (𝑥
·R 𝑧) ∈ R) |
7 | | m1r 7672 |
. . . . . 6
⊢
-1R ∈ R |
8 | | mulclsr 7674 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R)
→ (𝑦
·R 𝑤) ∈ R) |
9 | | mulclsr 7674 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R 𝑤) ∈ R) →
(-1R ·R (𝑦
·R 𝑤)) ∈ R) |
10 | 7, 8, 9 | sylancr 411 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R)
→ (-1R ·R (𝑦
·R 𝑤)) ∈ R) |
11 | | addclsr 7673 |
. . . . 5
⊢ (((𝑥
·R 𝑧) ∈ R ∧
(-1R ·R (𝑦
·R 𝑤)) ∈ R) → ((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
12 | 6, 10, 11 | syl2an 287 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑧 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑤
∈ R)) → ((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
13 | 12 | an4s 578 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R) |
14 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
𝑧 ∈ R)
→ (𝑦
·R 𝑧) ∈ R) |
15 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
𝑤 ∈ R)
→ (𝑥
·R 𝑤) ∈ R) |
16 | | addclsr 7673 |
. . . . 5
⊢ (((𝑦
·R 𝑧) ∈ R ∧ (𝑥
·R 𝑤) ∈ R) → ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R) |
17 | 14, 15, 16 | syl2anr 288 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑤 ∈ R)
∧ (𝑦 ∈
R ∧ 𝑧
∈ R)) → ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ∈ R) |
18 | 17 | an42s 579 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → ((𝑦 ·R 𝑧) +R
(𝑥
·R 𝑤)) ∈ R) |
19 | 13, 18 | jca 304 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R)) → (((𝑥 ·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ∈ R ∧ ((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ∈ R)) |
20 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑣 ∈ R)
→ (𝑧
·R 𝑣) ∈ R) |
21 | | mulclsr 7674 |
. . . . . 6
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (𝑤
·R 𝑢) ∈ R) |
22 | | mulclsr 7674 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑤
·R 𝑢) ∈ R) →
(-1R ·R (𝑤
·R 𝑢)) ∈ R) |
23 | 7, 21, 22 | sylancr 411 |
. . . . 5
⊢ ((𝑤 ∈ R ∧
𝑢 ∈ R)
→ (-1R ·R (𝑤
·R 𝑢)) ∈ R) |
24 | | addclsr 7673 |
. . . . 5
⊢ (((𝑧
·R 𝑣) ∈ R ∧
(-1R ·R (𝑤
·R 𝑢)) ∈ R) → ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
25 | 20, 23, 24 | syl2an 287 |
. . . 4
⊢ (((𝑧 ∈ R ∧
𝑣 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
26 | 25 | an4s 578 |
. . 3
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R) |
27 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑤 ∈ R ∧
𝑣 ∈ R)
→ (𝑤
·R 𝑣) ∈ R) |
28 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑧 ∈ R ∧
𝑢 ∈ R)
→ (𝑧
·R 𝑢) ∈ R) |
29 | | addclsr 7673 |
. . . . 5
⊢ (((𝑤
·R 𝑣) ∈ R ∧ (𝑧
·R 𝑢) ∈ R) → ((𝑤
·R 𝑣) +R (𝑧
·R 𝑢)) ∈ R) |
30 | 27, 28, 29 | syl2anr 288 |
. . . 4
⊢ (((𝑧 ∈ R ∧
𝑢 ∈ R)
∧ (𝑤 ∈
R ∧ 𝑣
∈ R)) → ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)) ∈ R) |
31 | 30 | an42s 579 |
. . 3
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)) ∈ R) |
32 | 26, 31 | jca 304 |
. 2
⊢ (((𝑧 ∈ R ∧
𝑤 ∈ R)
∧ (𝑣 ∈
R ∧ 𝑢
∈ R)) → (((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢))) ∈ R ∧ ((𝑤
·R 𝑣) +R (𝑧
·R 𝑢)) ∈ R)) |
33 | | simp1l 1006 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑥 ∈
R) |
34 | | simp2l 1008 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑧 ∈
R) |
35 | | simp3l 1010 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑣 ∈
R) |
36 | 34, 35, 20 | syl2anc 409 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑧
·R 𝑣) ∈ R) |
37 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
(𝑧
·R 𝑣) ∈ R) → (𝑥
·R (𝑧 ·R 𝑣)) ∈
R) |
38 | 33, 36, 37 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (𝑧 ·R 𝑣)) ∈
R) |
39 | | simp2r 1009 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑤 ∈
R) |
40 | | simp3r 1011 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑢 ∈
R) |
41 | 39, 40, 21 | syl2anc 409 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑤
·R 𝑢) ∈ R) |
42 | 7, 41, 22 | sylancr 411 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑤
·R 𝑢)) ∈ R) |
43 | | mulclsr 7674 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
(-1R ·R (𝑤
·R 𝑢)) ∈ R) → (𝑥
·R (-1R
·R (𝑤 ·R 𝑢))) ∈
R) |
44 | 33, 42, 43 | syl2anc 409 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (-1R
·R (𝑤 ·R 𝑢))) ∈
R) |
45 | | simp1r 1007 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
𝑦 ∈
R) |
46 | 39, 35, 27 | syl2anc 409 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑤
·R 𝑣) ∈ R) |
47 | | mulclsr 7674 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
(𝑤
·R 𝑣) ∈ R) → (𝑦
·R (𝑤 ·R 𝑣)) ∈
R) |
48 | 45, 46, 47 | syl2anc 409 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R (𝑤 ·R 𝑣)) ∈
R) |
49 | | mulclsr 7674 |
. . . . 5
⊢
((-1R ∈ R ∧ (𝑦
·R (𝑤 ·R 𝑣)) ∈ R)
→ (-1R ·R (𝑦
·R (𝑤 ·R 𝑣))) ∈
R) |
50 | 7, 48, 49 | sylancr 411 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R (𝑤 ·R 𝑣))) ∈
R) |
51 | | addcomsrg 7675 |
. . . . 5
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
+R 𝑔) = (𝑔 +R 𝑓)) |
52 | 51 | adantl 275 |
. . . 4
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
+R 𝑔) = (𝑔 +R 𝑓)) |
53 | | addasssrg 7676 |
. . . . 5
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
+R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R
ℎ))) |
54 | 53 | adantl 275 |
. . . 4
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R ∧ ℎ
∈ R)) → ((𝑓 +R 𝑔) +R
ℎ) = (𝑓 +R (𝑔 +R
ℎ))) |
55 | 34, 40, 28 | syl2anc 409 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑧
·R 𝑢) ∈ R) |
56 | | mulclsr 7674 |
. . . . . 6
⊢ ((𝑦 ∈ R ∧
(𝑧
·R 𝑢) ∈ R) → (𝑦
·R (𝑧 ·R 𝑢)) ∈
R) |
57 | 45, 55, 56 | syl2anc 409 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R (𝑧 ·R 𝑢)) ∈
R) |
58 | | mulclsr 7674 |
. . . . 5
⊢
((-1R ∈ R ∧ (𝑦
·R (𝑧 ·R 𝑢)) ∈ R)
→ (-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) ∈
R) |
59 | 7, 57, 58 | sylancr 411 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) ∈
R) |
60 | | addclsr 7673 |
. . . . 5
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
+R 𝑔) ∈ R) |
61 | 60 | adantl 275 |
. . . 4
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
+R 𝑔) ∈ R) |
62 | 38, 44, 50, 52, 54, 59, 61 | caov42d 6007 |
. . 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 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 ·R 𝑣)))) +R
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(𝑥
·R (-1R
·R (𝑤 ·R 𝑢)))))) |
63 | | distrsrg 7679 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
(𝑧
·R 𝑣) ∈ R ∧
(-1R ·R (𝑤
·R 𝑢)) ∈ R) → (𝑥
·R ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) = ((𝑥 ·R (𝑧
·R 𝑣)) +R (𝑥
·R (-1R
·R (𝑤 ·R 𝑢))))) |
64 | 33, 36, 42, 63 | syl3anc 1220 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) = ((𝑥 ·R (𝑧
·R 𝑣)) +R (𝑥
·R (-1R
·R (𝑤 ·R 𝑢))))) |
65 | | distrsrg 7679 |
. . . . . . 7
⊢ ((𝑦 ∈ R ∧
(𝑤
·R 𝑣) ∈ R ∧ (𝑧
·R 𝑢) ∈ R) → (𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))) = ((𝑦 ·R (𝑤
·R 𝑣)) +R (𝑦
·R (𝑧 ·R 𝑢)))) |
66 | 45, 46, 55, 65 | syl3anc 1220 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))) = ((𝑦 ·R (𝑤
·R 𝑣)) +R (𝑦
·R (𝑧 ·R 𝑢)))) |
67 | 66 | oveq2d 5840 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)))) = (-1R
·R ((𝑦 ·R (𝑤
·R 𝑣)) +R (𝑦
·R (𝑧 ·R 𝑢))))) |
68 | 7 | a1i 9 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
-1R ∈ R) |
69 | | distrsrg 7679 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R (𝑤 ·R 𝑣)) ∈ R ∧
(𝑦
·R (𝑧 ·R 𝑢)) ∈ R)
→ (-1R ·R ((𝑦
·R (𝑤 ·R 𝑣)) +R
(𝑦
·R (𝑧 ·R 𝑢)))) =
((-1R ·R (𝑦
·R (𝑤 ·R 𝑣))) +R
(-1R ·R (𝑦
·R (𝑧 ·R 𝑢))))) |
70 | 68, 48, 57, 69 | syl3anc 1220 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R ((𝑦
·R (𝑤 ·R 𝑣)) +R
(𝑦
·R (𝑧 ·R 𝑢)))) =
((-1R ·R (𝑦
·R (𝑤 ·R 𝑣))) +R
(-1R ·R (𝑦
·R (𝑧 ·R 𝑢))))) |
71 | 67, 70 | eqtrd 2190 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)))) = ((-1R
·R (𝑦 ·R (𝑤
·R 𝑣))) +R
(-1R ·R (𝑦
·R (𝑧 ·R 𝑢))))) |
72 | 64, 71 | oveq12d 5842 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑥
·R ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) +R
(-1R ·R (𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))))) = (((𝑥 ·R (𝑧
·R 𝑣)) +R (𝑥
·R (-1R
·R (𝑤 ·R 𝑢)))) +R
((-1R ·R (𝑦
·R (𝑤 ·R 𝑣))) +R
(-1R ·R (𝑦
·R (𝑧 ·R 𝑢)))))) |
73 | | mulcomsrg 7677 |
. . . . . . 7
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
·R 𝑔) = (𝑔 ·R 𝑓)) |
74 | 73 | adantl 275 |
. . . . . 6
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
·R 𝑔) = (𝑔 ·R 𝑓)) |
75 | | distrsrg 7679 |
. . . . . . . . 9
⊢ ((ℎ ∈ R ∧
𝑓 ∈ R
∧ 𝑔 ∈
R) → (ℎ
·R (𝑓 +R 𝑔)) = ((ℎ ·R 𝑓) +R
(ℎ
·R 𝑔))) |
76 | 75 | 3coml 1192 |
. . . . . . . 8
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → (ℎ
·R (𝑓 +R 𝑔)) = ((ℎ ·R 𝑓) +R
(ℎ
·R 𝑔))) |
77 | | simp3 984 |
. . . . . . . . 9
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ℎ
∈ R) |
78 | 60 | 3adant3 1002 |
. . . . . . . . 9
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → (𝑓
+R 𝑔) ∈ R) |
79 | | mulcomsrg 7677 |
. . . . . . . . 9
⊢ ((ℎ ∈ R ∧
(𝑓
+R 𝑔) ∈ R) → (ℎ
·R (𝑓 +R 𝑔)) = ((𝑓 +R 𝑔)
·R ℎ)) |
80 | 77, 78, 79 | syl2anc 409 |
. . . . . . . 8
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → (ℎ
·R (𝑓 +R 𝑔)) = ((𝑓 +R 𝑔)
·R ℎ)) |
81 | | simp1 982 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → 𝑓
∈ R) |
82 | | mulcomsrg 7677 |
. . . . . . . . . 10
⊢ ((ℎ ∈ R ∧
𝑓 ∈ R)
→ (ℎ
·R 𝑓) = (𝑓 ·R ℎ)) |
83 | 77, 81, 82 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → (ℎ
·R 𝑓) = (𝑓 ·R ℎ)) |
84 | | simp2 983 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → 𝑔
∈ R) |
85 | | mulcomsrg 7677 |
. . . . . . . . . 10
⊢ ((ℎ ∈ R ∧
𝑔 ∈ R)
→ (ℎ
·R 𝑔) = (𝑔 ·R ℎ)) |
86 | 77, 84, 85 | syl2anc 409 |
. . . . . . . . 9
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → (ℎ
·R 𝑔) = (𝑔 ·R ℎ)) |
87 | 83, 86 | oveq12d 5842 |
. . . . . . . 8
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((ℎ
·R 𝑓) +R (ℎ
·R 𝑔)) = ((𝑓 ·R ℎ) +R
(𝑔
·R ℎ))) |
88 | 76, 80, 87 | 3eqtr3d 2198 |
. . . . . . 7
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
+R 𝑔) ·R ℎ) = ((𝑓 ·R ℎ) +R
(𝑔
·R ℎ))) |
89 | 88 | adantl 275 |
. . . . . 6
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R ∧ ℎ
∈ R)) → ((𝑓 +R 𝑔)
·R ℎ) = ((𝑓 ·R ℎ) +R
(𝑔
·R ℎ))) |
90 | | mulasssrg 7678 |
. . . . . . 7
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R
∧ ℎ ∈
R) → ((𝑓
·R 𝑔) ·R ℎ) = (𝑓 ·R (𝑔
·R ℎ))) |
91 | 90 | adantl 275 |
. . . . . 6
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R ∧ ℎ
∈ R)) → ((𝑓 ·R 𝑔)
·R ℎ) = (𝑓 ·R (𝑔
·R ℎ))) |
92 | | mulclsr 7674 |
. . . . . . 7
⊢ ((𝑓 ∈ R ∧
𝑔 ∈ R)
→ (𝑓
·R 𝑔) ∈ R) |
93 | 92 | adantl 275 |
. . . . . 6
⊢ ((((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) ∧
(𝑓 ∈ R
∧ 𝑔 ∈
R)) → (𝑓
·R 𝑔) ∈ R) |
94 | 45, 39, 8 | syl2anc 409 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R 𝑤) ∈ R) |
95 | 74, 89, 91, 93, 33, 68, 34, 94, 35 | caovdilemd 6012 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑣) = ((𝑥 ·R (𝑧
·R 𝑣)) +R
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑣)))) |
96 | | mulasssrg 7678 |
. . . . . . . 8
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R
∧ 𝑣 ∈
R) → ((𝑦
·R 𝑤) ·R 𝑣) = (𝑦 ·R (𝑤
·R 𝑣))) |
97 | 45, 39, 35, 96 | syl3anc 1220 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑦
·R 𝑤) ·R 𝑣) = (𝑦 ·R (𝑤
·R 𝑣))) |
98 | 97 | oveq2d 5840 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑣)) =
(-1R ·R (𝑦
·R (𝑤 ·R 𝑣)))) |
99 | 98 | oveq2d 5840 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑥
·R (𝑧 ·R 𝑣)) +R
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑣))) = ((𝑥 ·R (𝑧
·R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 ·R 𝑣))))) |
100 | 95, 99 | eqtrd 2190 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑣) = ((𝑥 ·R (𝑧
·R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 ·R 𝑣))))) |
101 | 74, 89, 91, 93, 45, 33, 34, 39, 40 | caovdilemd 6012 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑢) = ((𝑦 ·R (𝑧
·R 𝑢)) +R (𝑥
·R (𝑤 ·R 𝑢)))) |
102 | 101 | oveq2d 5840 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑢)) =
(-1R ·R ((𝑦
·R (𝑧 ·R 𝑢)) +R
(𝑥
·R (𝑤 ·R 𝑢))))) |
103 | 93, 33, 41 | caovcld 5974 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (𝑤 ·R 𝑢)) ∈
R) |
104 | | distrsrg 7679 |
. . . . . 6
⊢
((-1R ∈ R ∧ (𝑦
·R (𝑧 ·R 𝑢)) ∈ R ∧
(𝑥
·R (𝑤 ·R 𝑢)) ∈ R)
→ (-1R ·R ((𝑦
·R (𝑧 ·R 𝑢)) +R
(𝑥
·R (𝑤 ·R 𝑢)))) =
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(-1R ·R (𝑥
·R (𝑤 ·R 𝑢))))) |
105 | 68, 57, 103, 104 | syl3anc 1220 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R ((𝑦
·R (𝑧 ·R 𝑢)) +R
(𝑥
·R (𝑤 ·R 𝑢)))) =
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(-1R ·R (𝑥
·R (𝑤 ·R 𝑢))))) |
106 | 68, 33, 41, 74, 91 | caov12d 6002 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑥
·R (𝑤 ·R 𝑢))) = (𝑥 ·R
(-1R ·R (𝑤
·R 𝑢)))) |
107 | 106 | oveq2d 5840 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(-1R ·R (𝑥
·R (𝑤 ·R 𝑢)))) =
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(𝑥
·R (-1R
·R (𝑤 ·R 𝑢))))) |
108 | 102, 105,
107 | 3eqtrd 2194 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑢)) =
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(𝑥
·R (-1R
·R (𝑤 ·R 𝑢))))) |
109 | 100, 108 | oveq12d 5842 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑣) +R
(-1R ·R (((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑢))) = (((𝑥 ·R (𝑧
·R 𝑣)) +R
(-1R ·R (𝑦
·R (𝑤 ·R 𝑣)))) +R
((-1R ·R (𝑦
·R (𝑧 ·R 𝑢))) +R
(𝑥
·R (-1R
·R (𝑤 ·R 𝑢)))))) |
110 | 62, 72, 109 | 3eqtr4rd 2201 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑣) +R
(-1R ·R (((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑢))) = ((𝑥 ·R ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) +R
(-1R ·R (𝑦
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)))))) |
111 | 93, 45, 36 | caovcld 5974 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R (𝑧 ·R 𝑣)) ∈
R) |
112 | 93, 45, 42 | caovcld 5974 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R (-1R
·R (𝑤 ·R 𝑢))) ∈
R) |
113 | 93, 33, 46 | caovcld 5974 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (𝑤 ·R 𝑣)) ∈
R) |
114 | 93, 33, 55 | caovcld 5974 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R (𝑧 ·R 𝑢)) ∈
R) |
115 | 111, 112,
113, 52, 54, 114, 61 | caov42d 6007 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑦
·R (𝑧 ·R 𝑣)) +R
(𝑦
·R (-1R
·R (𝑤 ·R 𝑢)))) +R
((𝑥
·R (𝑤 ·R 𝑣)) +R
(𝑥
·R (𝑧 ·R 𝑢)))) = (((𝑦 ·R (𝑧
·R 𝑣)) +R (𝑥
·R (𝑤 ·R 𝑣))) +R
((𝑥
·R (𝑧 ·R 𝑢)) +R
(𝑦
·R (-1R
·R (𝑤 ·R 𝑢)))))) |
116 | | distrsrg 7679 |
. . . . 5
⊢ ((𝑦 ∈ R ∧
(𝑧
·R 𝑣) ∈ R ∧
(-1R ·R (𝑤
·R 𝑢)) ∈ R) → (𝑦
·R ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) = ((𝑦 ·R (𝑧
·R 𝑣)) +R (𝑦
·R (-1R
·R (𝑤 ·R 𝑢))))) |
117 | 45, 36, 42, 116 | syl3anc 1220 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑦
·R ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) = ((𝑦 ·R (𝑧
·R 𝑣)) +R (𝑦
·R (-1R
·R (𝑤 ·R 𝑢))))) |
118 | | distrsrg 7679 |
. . . . 5
⊢ ((𝑥 ∈ R ∧
(𝑤
·R 𝑣) ∈ R ∧ (𝑧
·R 𝑢) ∈ R) → (𝑥
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))) = ((𝑥 ·R (𝑤
·R 𝑣)) +R (𝑥
·R (𝑧 ·R 𝑢)))) |
119 | 33, 46, 55, 118 | syl3anc 1220 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(𝑥
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))) = ((𝑥 ·R (𝑤
·R 𝑣)) +R (𝑥
·R (𝑧 ·R 𝑢)))) |
120 | 117, 119 | oveq12d 5842 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑦
·R ((𝑧 ·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) +R (𝑥
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢)))) = (((𝑦 ·R (𝑧
·R 𝑣)) +R (𝑦
·R (-1R
·R (𝑤 ·R 𝑢)))) +R
((𝑥
·R (𝑤 ·R 𝑣)) +R
(𝑥
·R (𝑧 ·R 𝑢))))) |
121 | 74, 89, 91, 93, 45, 33, 34, 39, 35 | caovdilemd 6012 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑣) = ((𝑦 ·R (𝑧
·R 𝑣)) +R (𝑥
·R (𝑤 ·R 𝑣)))) |
122 | 74, 89, 91, 93, 33, 68, 34, 94, 40 | caovdilemd 6012 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑢) = ((𝑥 ·R (𝑧
·R 𝑢)) +R
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑢)))) |
123 | | mulasssrg 7678 |
. . . . . . . . 9
⊢ ((𝑦 ∈ R ∧
𝑤 ∈ R
∧ 𝑢 ∈
R) → ((𝑦
·R 𝑤) ·R 𝑢) = (𝑦 ·R (𝑤
·R 𝑢))) |
124 | 45, 39, 40, 123 | syl3anc 1220 |
. . . . . . . 8
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑦
·R 𝑤) ·R 𝑢) = (𝑦 ·R (𝑤
·R 𝑢))) |
125 | 124 | oveq2d 5840 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑢)) =
(-1R ·R (𝑦
·R (𝑤 ·R 𝑢)))) |
126 | 68, 45, 41, 74, 91 | caov12d 6002 |
. . . . . . 7
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R (𝑦
·R (𝑤 ·R 𝑢))) = (𝑦 ·R
(-1R ·R (𝑤
·R 𝑢)))) |
127 | 125, 126 | eqtrd 2190 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑢)) = (𝑦 ·R
(-1R ·R (𝑤
·R 𝑢)))) |
128 | 127 | oveq2d 5840 |
. . . . 5
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((𝑥
·R (𝑧 ·R 𝑢)) +R
(-1R ·R ((𝑦
·R 𝑤) ·R 𝑢))) = ((𝑥 ·R (𝑧
·R 𝑢)) +R (𝑦
·R (-1R
·R (𝑤 ·R 𝑢))))) |
129 | 122, 128 | eqtrd 2190 |
. . . 4
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑢) = ((𝑥 ·R (𝑧
·R 𝑢)) +R (𝑦
·R (-1R
·R (𝑤 ·R 𝑢))))) |
130 | 121, 129 | oveq12d 5842 |
. . 3
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑣) +R
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑢)) = (((𝑦 ·R (𝑧
·R 𝑣)) +R (𝑥
·R (𝑤 ·R 𝑣))) +R
((𝑥
·R (𝑧 ·R 𝑢)) +R
(𝑦
·R (-1R
·R (𝑤 ·R 𝑢)))))) |
131 | 115, 120,
130 | 3eqtr4rd 2201 |
. 2
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ (𝑧 ∈
R ∧ 𝑤
∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) →
((((𝑦
·R 𝑧) +R (𝑥
·R 𝑤)) ·R 𝑣) +R
(((𝑥
·R 𝑧) +R
(-1R ·R (𝑦
·R 𝑤))) ·R 𝑢)) = ((𝑦 ·R ((𝑧
·R 𝑣) +R
(-1R ·R (𝑤
·R 𝑢)))) +R (𝑥
·R ((𝑤 ·R 𝑣) +R
(𝑧
·R 𝑢))))) |
132 | 1, 2, 3, 4, 5, 19,
32, 110, 131 | ecoviass 6590 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))) |