HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axmulass 5201
Description: Multiplication of complex numbers is associative. Axiom 12 of 25 for real and complex numbers, derived from ZF set theory.
Assertion
Ref Expression
axmulass |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A x. B) x. C) = (A x. (B x. C)))
Proof of Theorem axmulass
StepHypRef Expression
1 dfcnqs 5185 . 2 |- CC = ((R. X. R.)/.`'E)
2 mulcnsrec 5187 . 2 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ([<.x, y>.]`'E x. [<.z, w>.]`'E) = [<.((x .R z) +R (-1R .R (y .R w))), ((y .R z) +R (x .R w))>.]`'E)
3 mulcnsrec 5187 . 2 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> ([<.z, w>.]`'E x. [<.v, u>.]`'E) = [<.((z .R v) +R (-1R .R (w .R u))), ((w .R v) +R (z .R u))>.]`'E)
4 mulcnsrec 5187 . 2 |- (((((x .R z) +R (-1R .R (y .R w))) e. R. /\ ((y .R z) +R (x .R w)) e. R.) /\ (v e. R. /\ u e. R.)) -> ([<.((x .R z) +R (-1R .R (y .R w))), ((y .R z) +R (x .R w))>.]`'E x. [<.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 5187 . 2 |- (((x e. R. /\ y e. R.) /\ (((z .R v) +R (-1R .R (w .R u))) e. R. /\ ((w .R v) +R (z .R u)) e. R.)) -> ([<.x, y>.]`'E x. [<.((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 addclsr 5115 . . . . 5 |- (((x .R z) e. R. /\ (-1R .R (y .R w)) e. R.) -> ((x .R z) +R (-1R .R (y .R w))) e. R.)
7 mulclsr 5116 . . . . 5 |- ((x e. R. /\ z e. R.) -> (x .R z) e. R.)
8 mulclsr 5116 . . . . . 6 |- ((y e. R. /\ w e. R.) -> (y .R w) e. R.)
9 m1r 5114 . . . . . . 7 |- -1R e. R.
10 mulclsr 5116 . . . . . . 7 |- ((-1R e. R. /\ (y .R w) e. R.) -> (-1R .R (y .R w)) e. R.)
119, 10mpan 692 . . . . . 6 |- ((y .R w) e. R. -> (-1R .R (y .R w)) e. R.)
128, 11syl 10 . . . . 5 |- ((y e. R. /\ w e. R.) -> (-1R .R (y .R w)) e. R.)
136, 7, 12syl2an 454 . . . 4 |- (((x e. R. /\ z e. R.) /\ (y e. R. /\ w e. R.)) -> ((x .R z) +R (-1R .R (y .R w))) e. R.)
1413an4s 507 . . 3 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ((x .R z) +R (-1R .R (y .R w))) e. R.)
15 addclsr 5115 . . . . . 6 |- (((y .R z) e. R. /\ (x .R w) e. R.) -> ((y .R z) +R (x .R w)) e. R.)
16 mulclsr 5116 . . . . . 6 |- ((y e. R. /\ z e. R.) -> (y .R z) e. R.)
17 mulclsr 5116 . . . . . 6 |- ((x e. R. /\ w e. R.) -> (x .R w) e. R.)
1815, 16, 17syl2an 454 . . . . 5 |- (((y e. R. /\ z e. R.) /\ (x e. R. /\ w e. R.)) -> ((y .R z) +R (x .R w)) e. R.)
1918ancoms 436 . . . 4 |- (((x e. R. /\ w e. R.) /\ (y e. R. /\ z e. R.)) -> ((y .R z) +R (x .R w)) e. R.)
2019an42s 508 . . 3 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ((y .R z) +R (x .R w)) e. R.)
2114, 20jca 288 . 2 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> (((x .R z) +R (-1R .R (y .R w))) e. R. /\ ((y .R z) +R (x .R w)) e. R.))
22 addclsr 5115 . . . . 5 |- (((z .R v) e. R. /\ (-1R .R (w .R u)) e. R.) -> ((z .R v) +R (-1R .R (w .R u))) e. R.)
23 mulclsr 5116 . . . . 5 |- ((z e. R. /\ v e. R.) -> (z .R v) e. R.)
24 mulclsr 5116 . . . . . 6 |- ((w e. R. /\ u e. R.) -> (w .R u) e. R.)
25 mulclsr 5116 . . . . . . 7 |- ((-1R e. R. /\ (w .R u) e. R.) -> (-1R .R (w .R u)) e. R.)
269, 25mpan 692 . . . . . 6 |- ((w .R u) e. R. -> (-1R .R (w .R u)) e. R.)
2724, 26syl 10 . . . . 5 |- ((w e. R. /\ u e. R.) -> (-1R .R (w .R u)) e. R.)
2822, 23, 27syl2an 454 . . . 4 |- (((z e. R. /\ v e. R.) /\ (w e. R. /\ u e. R.)) -> ((z .R v) +R (-1R .R (w .R u))) e. R.)
2928an4s 507 . . 3 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> ((z .R v) +R (-1R .R (w .R u))) e. R.)
30 addclsr 5115 . . . . . 6 |- (((w .R v) e. R. /\ (z .R u) e. R.) -> ((w .R v) +R (z .R u)) e. R.)
31 mulclsr 5116 . . . . . 6 |- ((w e. R. /\ v e. R.) -> (w .R v) e. R.)
32 mulclsr 5116 . . . . . 6 |- ((z e. R. /\ u e. R.) -> (z .R u) e. R.)
3330, 31, 32syl2an 454 . . . . 5 |- (((w e. R. /\ v e. R.) /\ (z e. R. /\ u e. R.)) -> ((w .R v) +R (z .R u)) e. R.)
3433ancoms 436 . . . 4 |- (((z e. R. /\ u e. R.) /\ (w e. R. /\ v e. R.)) -> ((w .R v) +R (z .R u)) e. R.)
3534an42s 508 . . 3 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> ((w .R v) +R (z .R u)) e. R.)
3629, 35jca 288 . 2 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> (((z .R v) +R (-1R .R (w .R u))) e. R. /\ ((w .R v) +R (z .R u)) e. R.))
37 oprex 3922 . . . 4 |- (x .R (z .R v)) e. V
38 oprex 3922 . . . 4 |- (x .R (-1R .R (w .R u))) e. V
39 oprex 3922 . . . 4 |- (-1R .R (y .R (w .R v))) e. V
40 visset 1788 . . . . 5 |- f e. V
41 visset 1788 . . . . 5 |- g e. V
4240, 41addcomsr 5119 . . . 4 |- (f +R g) = (g +R f)
43 visset 1788 . . . . 5 |- h e. V
4441, 43addasssr 5120 . . . 4 |- ((f +R g) +R h) = (f +R (g +R h))
45 oprex 3922 . . . 4 |- (-1R .R (y .R (z .R u))) e. V
4637, 38, 39, 42, 44, 45caopr42 4006 . . 3 |- (((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)))))
47 oprex 3922 . . . . 5 |- (z .R v) e. V
48 oprex 3922 . . . . 5 |- (-1R .R (w .R u)) e. V
4947, 48distrsr 5123 . . . 4 |- (x .R ((z .R v) +R (-1R .R (w .R u)))) = ((x .R (z .R v)) +R (x .R (-1R .R (w .R u))))
50 oprex 3922 . . . . . . 7 |- (w .R v) e. V
51 oprex 3922 . . . . . . 7 |- (z .R u) e. V
5250, 51distrsr 5123 . . . . . 6 |- (y .R ((w .R v) +R (z .R u))) = ((y .R (w .R v)) +R (y .R (z .R u)))
5352opreq2i 3911 . . . . 5 |- (-1R .R (y .R ((w .R v) +R (z .R u)))) = (-1R .R ((y .R (w .R v)) +R (y .R (z .R u))))
54 oprex 3922 . . . . . 6 |- (y .R (w .R v)) e. V
55 oprex 3922 . . . . . 6 |- (y .R (z .R u)) e. V
5654, 55distrsr 5123 . . . . 5 |- (-1R .R