ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  axmulass Structured version   GIF version

Theorem axmulass 6717
Description: Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 6746. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
Assertion
Ref Expression
axmulass ((A B 𝐶 ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶)))

Proof of Theorem axmulass
Dummy variables x y z w v u f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfcnqs 6698 . 2 ℂ = ((R × R) / E )
2 mulcnsrec 6700 . 2 (((x R y R) (z R w R)) → ([⟨x, y⟩] E · [⟨z, w⟩] E ) = [⟨((x ·R z) +R (-1R ·R (y ·R w))), ((y ·R z) +R (x ·R w))⟩] E )
3 mulcnsrec 6700 . 2 (((z R w R) (v R u R)) → ([⟨z, w⟩] E · [⟨v, u⟩] E ) = [⟨((z ·R v) +R (-1R ·R (w ·R u))), ((w ·R v) +R (z ·R u))⟩] E )
4 mulcnsrec 6700 . 2 (((((x ·R z) +R (-1R ·R (y ·R w))) R ((y ·R z) +R (x ·R w)) R) (v R u R)) → ([⟨((x ·R z) +R (-1R ·R (y ·R w))), ((y ·R z) +R (x ·R w))⟩] E · [⟨v, u⟩] E ) = [⟨((((x ·R z) +R (-1R ·R (y ·R w))) ·R v) +R (-1R ·R (((y ·R z) +R (x ·R w)) ·R u))), ((((y ·R z) +R (x ·R w)) ·R v) +R (((x ·R z) +R (-1R ·R (y ·R w))) ·R u))⟩] E )
5 mulcnsrec 6700 . 2 (((x R y R) (((z ·R v) +R (-1R ·R (w ·R u))) R ((w ·R v) +R (z ·R u)) R)) → ([⟨x, y⟩] E · [⟨((z ·R v) +R (-1R ·R (w ·R u))), ((w ·R v) +R (z ·R u))⟩] E ) = [⟨((x ·R ((z ·R v) +R (-1R ·R (w ·R u)))) +R (-1R ·R (y ·R ((w ·R v) +R (z ·R u))))), ((y ·R ((z ·R v) +R (-1R ·R (w ·R u)))) +R (x ·R ((w ·R v) +R (z ·R u))))⟩] E )
6 mulclsr 6642 . . . . 5 ((x R z R) → (x ·R z) R)
7 m1r 6640 . . . . . 6 -1R R
8 mulclsr 6642 . . . . . 6 ((y R w R) → (y ·R w) R)
9 mulclsr 6642 . . . . . 6 ((-1R R (y ·R w) R) → (-1R ·R (y ·R w)) R)
107, 8, 9sylancr 393 . . . . 5 ((y R w R) → (-1R ·R (y ·R w)) R)
11 addclsr 6641 . . . . 5 (((x ·R z) R (-1R ·R (y ·R w)) R) → ((x ·R z) +R (-1R ·R (y ·R w))) R)
126, 10, 11syl2an 273 . . . 4 (((x R z R) (y R w R)) → ((x ·R z) +R (-1R ·R (y ·R w))) R)
1312an4s 522 . . 3 (((x R y R) (z R w R)) → ((x ·R z) +R (-1R ·R (y ·R w))) R)
14 mulclsr 6642 . . . . 5 ((y R z R) → (y ·R z) R)
15 mulclsr 6642 . . . . 5 ((x R w R) → (x ·R w) R)
16 addclsr 6641 . . . . 5 (((y ·R z) R (x ·R w) R) → ((y ·R z) +R (x ·R w)) R)
1714, 15, 16syl2anr 274 . . . 4 (((x R w R) (y R z R)) → ((y ·R z) +R (x ·R w)) R)
1817an42s 523 . . 3 (((x R y R) (z R w R)) → ((y ·R z) +R (x ·R w)) R)
1913, 18jca 290 . 2 (((x R y R) (z R w R)) → (((x ·R z) +R (-1R ·R (y ·R w))) R ((y ·R z) +R (x ·R w)) R))
20 mulclsr 6642 . . . . 5 ((z R v R) → (z ·R v) R)
21 mulclsr 6642 . . . . . 6 ((w R u R) → (w ·R u) R)
22 mulclsr 6642 . . . . . 6 ((-1R R (w ·R u) R) → (-1R ·R (w ·R u)) R)
237, 21, 22sylancr 393 . . . . 5 ((w R u R) → (-1R ·R (w ·R u)) R)
24 addclsr 6641 . . . . 5 (((z ·R v) R (-1R ·R (w ·R u)) R) → ((z ·R v) +R (-1R ·R (w ·R u))) R)
2520, 23, 24syl2an 273 . . . 4 (((z R v R) (w R u R)) → ((z ·R v) +R (-1R ·R (w ·R u))) R)
2625an4s 522 . . 3 (((z R w R) (v R u R)) → ((z ·R v) +R (-1R ·R (w ·R u))) R)
27 mulclsr 6642 . . . . 5 ((w R v R) → (w ·R v) R)
28 mulclsr 6642 . . . . 5 ((z R u R) → (z ·R u) R)
29 addclsr 6641 . . . . 5 (((w ·R v) R (z ·R u) R) → ((w ·R v) +R (z ·R u)) R)
3027, 28, 29syl2anr 274 . . . 4 (((z R u R) (w R v R)) → ((w ·R v) +R (z ·R u)) R)
3130an42s 523 . . 3 (((z R w R) (v R u R)) → ((w ·R v) +R (z ·R u)) R)
3226, 31jca 290 . 2 (((z R w R) (v R u R)) → (((z ·R v) +R (-1R ·R (w ·R u))) R ((w ·R v) +R (z ·R u)) R))
33 simp1l 927 . . . . 5 (((x R y R) (z R w R) (v R u R)) → x R)
34 simp2l 929 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → z R)
35 simp3l 931 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → v R)
3634, 35, 20syl2anc 391 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (z ·R v) R)
37 mulclsr 6642 . . . . 5 ((x R (z ·R v) R) → (x ·R (z ·R v)) R)
3833, 36, 37syl2anc 391 . . . 4 (((x R y R) (z R w R) (v R u R)) → (x ·R (z ·R v)) R)
39 simp2r 930 . . . . . . 7 (((x R y R) (z R w R) (v R u R)) → w R)
40 simp3r 932 . . . . . . 7 (((x R y R) (z R w R) (v R u R)) → u R)
4139, 40, 21syl2anc 391 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (w ·R u) R)
427, 41, 22sylancr 393 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (w ·R u)) R)
43 mulclsr 6642 . . . . 5 ((x R (-1R ·R (w ·R u)) R) → (x ·R (-1R ·R (w ·R u))) R)
4433, 42, 43syl2anc 391 . . . 4 (((x R y R) (z R w R) (v R u R)) → (x ·R (-1R ·R (w ·R u))) R)
45 simp1r 928 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → y R)
4639, 35, 27syl2anc 391 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (w ·R v) R)
47 mulclsr 6642 . . . . . 6 ((y R (w ·R v) R) → (y ·R (w ·R v)) R)
4845, 46, 47syl2anc 391 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (y ·R (w ·R v)) R)
49 mulclsr 6642 . . . . 5 ((-1R R (y ·R (w ·R v)) R) → (-1R ·R (y ·R (w ·R v))) R)
507, 48, 49sylancr 393 . . . 4 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (y ·R (w ·R v))) R)
51 addcomsrg 6643 . . . . 5 ((f R g R) → (f +R g) = (g +R f))
5251adantl 262 . . . 4 ((((x R y R) (z R w R) (v R u R)) (f R g R)) → (f +R g) = (g +R f))
53 addasssrg 6644 . . . . 5 ((f R g R R) → ((f +R g) +R ) = (f +R (g +R )))
5453adantl 262 . . . 4 ((((x R y R) (z R w R) (v R u R)) (f R g R R)) → ((f +R g) +R ) = (f +R (g +R )))
5534, 40, 28syl2anc 391 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (z ·R u) R)
56 mulclsr 6642 . . . . . 6 ((y R (z ·R u) R) → (y ·R (z ·R u)) R)
5745, 55, 56syl2anc 391 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (y ·R (z ·R u)) R)
58 mulclsr 6642 . . . . 5 ((-1R R (y ·R (z ·R u)) R) → (-1R ·R (y ·R (z ·R u))) R)
597, 57, 58sylancr 393 . . . 4 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (y ·R (z ·R u))) R)
60 addclsr 6641 . . . . 5 ((f R g R) → (f +R g) R)
6160adantl 262 . . . 4 ((((x R y R) (z R w R) (v R u R)) (f R g R)) → (f +R g) R)
6238, 44, 50, 52, 54, 59, 61caov42d 5629 . . 3 (((x R y R) (z R w R) (v R u R)) → (((x ·R (z ·R v)) +R (x ·R (-1R ·R (w ·R u)))) +R ((-1R ·R (y ·R (w ·R v))) +R (-1R ·R (y ·R (z ·R u))))) = (((x ·R (z ·R v)) +R (-1R ·R (y ·R (w ·R v)))) +R ((-1R ·R (y ·R (z ·R u))) +R (x ·R (-1R ·R (w ·R u))))))
63 distrsrg 6647 . . . . 5 ((x R (z ·R v) R (-1R ·R (w ·R u)) R) → (x ·R ((z ·R v) +R (-1R ·R (w ·R u)))) = ((x ·R (z ·R v)) +R (x ·R (-1R ·R (w ·R u)))))
6433, 36, 42, 63syl3anc 1134 . . . 4 (((x R y R) (z R w R) (v R u R)) → (x ·R ((z ·R v) +R (-1R ·R (w ·R u)))) = ((x ·R (z ·R v)) +R (x ·R (-1R ·R (w ·R u)))))
65 distrsrg 6647 . . . . . . 7 ((y R (w ·R v) R (z ·R u) R) → (y ·R ((w ·R v) +R (z ·R u))) = ((y ·R (w ·R v)) +R (y ·R (z ·R u))))
6645, 46, 55, 65syl3anc 1134 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (y ·R ((w ·R v) +R (z ·R u))) = ((y ·R (w ·R v)) +R (y ·R (z ·R u))))
6766oveq2d 5471 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (y ·R ((w ·R v) +R (z ·R u)))) = (-1R ·R ((y ·R (w ·R v)) +R (y ·R (z ·R u)))))
687a1i 9 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → -1R R)
69 distrsrg 6647 . . . . . 6 ((-1R R (y ·R (w ·R v)) R (y ·R (z ·R u)) R) → (-1R ·R ((y ·R (w ·R v)) +R (y ·R (z ·R u)))) = ((-1R ·R (y ·R (w ·R v))) +R (-1R ·R (y ·R (z ·R u)))))
7068, 48, 57, 69syl3anc 1134 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (-1R ·R ((y ·R (w ·R v)) +R (y ·R (z ·R u)))) = ((-1R ·R (y ·R (w ·R v))) +R (-1R ·R (y ·R (z ·R u)))))
7167, 70eqtrd 2069 . . . 4 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (y ·R ((w ·R v) +R (z ·R u)))) = ((-1R ·R (y ·R (w ·R v))) +R (-1R ·R (y ·R (z ·R u)))))
7264, 71oveq12d 5473 . . 3 (((x R y R) (z R w R) (v R u R)) → ((x ·R ((z ·R v) +R (-1R ·R (w ·R u)))) +R (-1R ·R (y ·R ((w ·R v) +R (z ·R u))))) = (((x ·R (z ·R v)) +R (x ·R (-1R ·R (w ·R u)))) +R ((-1R ·R (y ·R (w ·R v))) +R (-1R ·R (y ·R (z ·R u))))))
73 mulcomsrg 6645 . . . . . . 7 ((f R g R) → (f ·R g) = (g ·R f))
7473adantl 262 . . . . . 6 ((((x R y R) (z R w R) (v R u R)) (f R g R)) → (f ·R g) = (g ·R f))
75 distrsrg 6647 . . . . . . . . 9 (( R f R g R) → ( ·R (f +R g)) = (( ·R f) +R ( ·R g)))
76753coml 1110 . . . . . . . 8 ((f R g R R) → ( ·R (f +R g)) = (( ·R f) +R ( ·R g)))
77 simp3 905 . . . . . . . . 9 ((f R g R R) → R)
78603adant3 923 . . . . . . . . 9 ((f R g R R) → (f +R g) R)
79 mulcomsrg 6645 . . . . . . . . 9 (( R (f +R g) R) → ( ·R (f +R g)) = ((f +R g) ·R ))
8077, 78, 79syl2anc 391 . . . . . . . 8 ((f R g R R) → ( ·R (f +R g)) = ((f +R g) ·R ))
81 simp1 903 . . . . . . . . . 10 ((f R g R R) → f R)
82 mulcomsrg 6645 . . . . . . . . . 10 (( R f R) → ( ·R f) = (f ·R ))
8377, 81, 82syl2anc 391 . . . . . . . . 9 ((f R g R R) → ( ·R f) = (f ·R ))
84 simp2 904 . . . . . . . . . 10 ((f R g R R) → g R)
85 mulcomsrg 6645 . . . . . . . . . 10 (( R g R) → ( ·R g) = (g ·R ))
8677, 84, 85syl2anc 391 . . . . . . . . 9 ((f R g R R) → ( ·R g) = (g ·R ))
8783, 86oveq12d 5473 . . . . . . . 8 ((f R g R R) → (( ·R f) +R ( ·R g)) = ((f ·R ) +R (g ·R )))
8876, 80, 873eqtr3d 2077 . . . . . . 7 ((f R g R R) → ((f +R g) ·R ) = ((f ·R ) +R (g ·R )))
8988adantl 262 . . . . . 6 ((((x R y R) (z R w R) (v R u R)) (f R g R R)) → ((f +R g) ·R ) = ((f ·R ) +R (g ·R )))
90 mulasssrg 6646 . . . . . . 7 ((f R g R R) → ((f ·R g) ·R ) = (f ·R (g ·R )))
9190adantl 262 . . . . . 6 ((((x R y R) (z R w R) (v R u R)) (f R g R R)) → ((f ·R g) ·R ) = (f ·R (g ·R )))
92 mulclsr 6642 . . . . . . 7 ((f R g R) → (f ·R g) R)
9392adantl 262 . . . . . 6 ((((x R y R) (z R w R) (v R u R)) (f R g R)) → (f ·R g) R)
9445, 39, 8syl2anc 391 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (y ·R w) R)
9574, 89, 91, 93, 33, 68, 34, 94, 35caovdilemd 5634 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (((x ·R z) +R (-1R ·R (y ·R w))) ·R v) = ((x ·R (z ·R v)) +R (-1R ·R ((y ·R w) ·R v))))
96 mulasssrg 6646 . . . . . . . 8 ((y R w R v R) → ((y ·R w) ·R v) = (y ·R (w ·R v)))
9745, 39, 35, 96syl3anc 1134 . . . . . . 7 (((x R y R) (z R w R) (v R u R)) → ((y ·R w) ·R v) = (y ·R (w ·R v)))
9897oveq2d 5471 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (-1R ·R ((y ·R w) ·R v)) = (-1R ·R (y ·R (w ·R v))))
9998oveq2d 5471 . . . . 5 (((x R y R) (z R w R) (v R u R)) → ((x ·R (z ·R v)) +R (-1R ·R ((y ·R w) ·R v))) = ((x ·R (z ·R v)) +R (-1R ·R (y ·R (w ·R v)))))
10095, 99eqtrd 2069 . . . 4 (((x R y R) (z R w R) (v R u R)) → (((x ·R z) +R (-1R ·R (y ·R w))) ·R v) = ((x ·R (z ·R v)) +R (-1R ·R (y ·R (w ·R v)))))
10174, 89, 91, 93, 45, 33, 34, 39, 40caovdilemd 5634 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (((y ·R z) +R (x ·R w)) ·R u) = ((y ·R (z ·R u)) +R (x ·R (w ·R u))))
102101oveq2d 5471 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (((y ·R z) +R (x ·R w)) ·R u)) = (-1R ·R ((y ·R (z ·R u)) +R (x ·R (w ·R u)))))
10393, 33, 41caovcld 5596 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (x ·R (w ·R u)) R)
104 distrsrg 6647 . . . . . 6 ((-1R R (y ·R (z ·R u)) R (x ·R (w ·R u)) R) → (-1R ·R ((y ·R (z ·R u)) +R (x ·R (w ·R u)))) = ((-1R ·R (y ·R (z ·R u))) +R (-1R ·R (x ·R (w ·R u)))))
10568, 57, 103, 104syl3anc 1134 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (-1R ·R ((y ·R (z ·R u)) +R (x ·R (w ·R u)))) = ((-1R ·R (y ·R (z ·R u))) +R (-1R ·R (x ·R (w ·R u)))))
10668, 33, 41, 74, 91caov12d 5624 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (x ·R (w ·R u))) = (x ·R (-1R ·R (w ·R u))))
107106oveq2d 5471 . . . . 5 (((x R y R) (z R w R) (v R u R)) → ((-1R ·R (y ·R (z ·R u))) +R (-1R ·R (x ·R (w ·R u)))) = ((-1R ·R (y ·R (z ·R u))) +R (x ·R (-1R ·R (w ·R u)))))
108102, 105, 1073eqtrd 2073 . . . 4 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (((y ·R z) +R (x ·R w)) ·R u)) = ((-1R ·R (y ·R (z ·R u))) +R (x ·R (-1R ·R (w ·R u)))))
109100, 108oveq12d 5473 . . 3 (((x R y R) (z R w R) (v R u R)) → ((((x ·R z) +R (-1R ·R (y ·R w))) ·R v) +R (-1R ·R (((y ·R z) +R (x ·R w)) ·R u))) = (((x ·R (z ·R v)) +R (-1R ·R (y ·R (w ·R v)))) +R ((-1R ·R (y ·R (z ·R u))) +R (x ·R (-1R ·R (w ·R u))))))
11062, 72, 1093eqtr4rd 2080 . 2 (((x R y R) (z R w R) (v R u R)) → ((((x ·R z) +R (-1R ·R (y ·R w))) ·R v) +R (-1R ·R (((y ·R z) +R (x ·R w)) ·R u))) = ((x ·R ((z ·R v) +R (-1R ·R (w ·R u)))) +R (-1R ·R (y ·R ((w ·R v) +R (z ·R u))))))
11193, 45, 36caovcld 5596 . . . 4 (((x R y R) (z R w R) (v R u R)) → (y ·R (z ·R v)) R)
11293, 45, 42caovcld 5596 . . . 4 (((x R y R) (z R w R) (v R u R)) → (y ·R (-1R ·R (w ·R u))) R)
11393, 33, 46caovcld 5596 . . . 4 (((x R y R) (z R w R) (v R u R)) → (x ·R (w ·R v)) R)
11493, 33, 55caovcld 5596 . . . 4 (((x R y R) (z R w R) (v R u R)) → (x ·R (z ·R u)) R)
115111, 112, 113, 52, 54, 114, 61caov42d 5629 . . 3 (((x R y R) (z R w R) (v R u R)) → (((y ·R (z ·R v)) +R (y ·R (-1R ·R (w ·R u)))) +R ((x ·R (w ·R v)) +R (x ·R (z ·R u)))) = (((y ·R (z ·R v)) +R (x ·R (w ·R v))) +R ((x ·R (z ·R u)) +R (y ·R (-1R ·R (w ·R u))))))
116 distrsrg 6647 . . . . 5 ((y R (z ·R v) R (-1R ·R (w ·R u)) R) → (y ·R ((z ·R v) +R (-1R ·R (w ·R u)))) = ((y ·R (z ·R v)) +R (y ·R (-1R ·R (w ·R u)))))
11745, 36, 42, 116syl3anc 1134 . . . 4 (((x R y R) (z R w R) (v R u R)) → (y ·R ((z ·R v) +R (-1R ·R (w ·R u)))) = ((y ·R (z ·R v)) +R (y ·R (-1R ·R (w ·R u)))))
118 distrsrg 6647 . . . . 5 ((x R (w ·R v) R (z ·R u) R) → (x ·R ((w ·R v) +R (z ·R u))) = ((x ·R (w ·R v)) +R (x ·R (z ·R u))))
11933, 46, 55, 118syl3anc 1134 . . . 4 (((x R y R) (z R w R) (v R u R)) → (x ·R ((w ·R v) +R (z ·R u))) = ((x ·R (w ·R v)) +R (x ·R (z ·R u))))
120117, 119oveq12d 5473 . . 3 (((x R y R) (z R w R) (v R u R)) → ((y ·R ((z ·R v) +R (-1R ·R (w ·R u)))) +R (x ·R ((w ·R v) +R (z ·R u)))) = (((y ·R (z ·R v)) +R (y ·R (-1R ·R (w ·R u)))) +R ((x ·R (w ·R v)) +R (x ·R (z ·R u)))))
12174, 89, 91, 93, 45, 33, 34, 39, 35caovdilemd 5634 . . . 4 (((x R y R) (z R w R) (v R u R)) → (((y ·R z) +R (x ·R w)) ·R v) = ((y ·R (z ·R v)) +R (x ·R (w ·R v))))
12274, 89, 91, 93, 33, 68, 34, 94, 40caovdilemd 5634 . . . . 5 (((x R y R) (z R w R) (v R u R)) → (((x ·R z) +R (-1R ·R (y ·R w))) ·R u) = ((x ·R (z ·R u)) +R (-1R ·R ((y ·R w) ·R u))))
123 mulasssrg 6646 . . . . . . . . 9 ((y R w R u R) → ((y ·R w) ·R u) = (y ·R (w ·R u)))
12445, 39, 40, 123syl3anc 1134 . . . . . . . 8 (((x R y R) (z R w R) (v R u R)) → ((y ·R w) ·R u) = (y ·R (w ·R u)))
125124oveq2d 5471 . . . . . . 7 (((x R y R) (z R w R) (v R u R)) → (-1R ·R ((y ·R w) ·R u)) = (-1R ·R (y ·R (w ·R u))))
12668, 45, 41, 74, 91caov12d 5624 . . . . . . 7 (((x R y R) (z R w R) (v R u R)) → (-1R ·R (y ·R (w ·R u))) = (y ·R (-1R ·R (w ·R u))))
127125, 126eqtrd 2069 . . . . . 6 (((x R y R) (z R w R) (v R u R)) → (-1R ·R ((y ·R w) ·R u)) = (y ·R (-1R ·R (w ·R u))))
128127oveq2d 5471 . . . . 5 (((x R y R) (z R w R) (v R u R)) → ((x ·R (z ·R u)) +R (-1R ·R ((y ·R w) ·R u))) = ((x ·R (z ·R u)) +R (y ·R (-1R ·R (w ·R u)))))
129122, 128eqtrd 2069 . . . 4 (((x R y R) (z R w R) (v R u R)) → (((x ·R z) +R (-1R ·R (y ·R w))) ·R u) = ((x ·R (z ·R u)) +R (y ·R (-1R ·R (w ·R u)))))
130121, 129oveq12d 5473 . . 3 (((x R y R) (z R w R) (v R u R)) → ((((y ·R z) +R (x ·R w)) ·R v) +R (((x ·R z) +R (-1R ·R (y ·R w))) ·R u)) = (((y ·R (z ·R v)) +R (x ·R (w ·R v))) +R ((x ·R (z ·R u)) +R (y ·R (-1R ·R (w ·R u))))))
131115, 120, 1303eqtr4rd 2080 . 2 (((x R y R) (z R w R) (v R u R)) → ((((y ·R z) +R (x ·R w)) ·R v) +R (((x ·R z) +R (-1R ·R (y ·R w))) ·R u)) = ((y ·R ((z ·R v) +R (-1R ·R (w ·R u)))) +R (x ·R ((w ·R v) +R (z ·R u)))))
1321, 2, 3, 4, 5, 19, 32, 110, 131ecoviass 6152 1 ((A B 𝐶 ℂ) → ((A · B) · 𝐶) = (A · (B · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884   = wceq 1242   wcel 1390   E cep 4015  ccnv 4287  (class class class)co 5455  Rcnr 6281  -1Rcm1r 6284   +R cplr 6285   ·R cmr 6286  cc 6669   · cmul 6676
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-eprel 4017  df-id 4021  df-po 4024  df-iso 4025  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-2o 5941  df-oadd 5944  df-omul 5945  df-er 6042  df-ec 6044  df-qs 6048  df-ni 6288  df-pli 6289  df-mi 6290  df-lti 6291  df-plpq 6328  df-mpq 6329  df-enq 6331  df-nqqs 6332  df-plqqs 6333  df-mqqs 6334  df-1nqqs 6335  df-rq 6336  df-ltnqqs 6337  df-enq0 6406  df-nq0 6407  df-0nq0 6408  df-plq0 6409  df-mq0 6410  df-inp 6448  df-i1p 6449  df-iplp 6450  df-imp 6451  df-enr 6614  df-nr 6615  df-plr 6616  df-mr 6617  df-m1r 6621  df-c 6677  df-mul 6683
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator