Metamath Proof Explorer

Theorem axmulass

Description: Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass . (Contributed by NM, 3-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion axmulass 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Proof

Step Hyp Ref Expression
1 dfcnqs 
 |-  CC = ( ( R. X. R. ) /. `' _E )
2 mulcnsrec 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( 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 mulclsr 
 |-  ( ( x e. R. /\ z e. R. ) -> ( x .R z ) e. R. )
7 m1r 
 |-  -1R e. R.
8 mulclsr 
 |-  ( ( y e. R. /\ w e. R. ) -> ( y .R w ) e. R. )
9 mulclsr 
 |-  ( ( -1R e. R. /\ ( y .R w ) e. R. ) -> ( -1R .R ( y .R w ) ) e. R. )
10 7 8 9 sylancr 
 |-  ( ( y e. R. /\ w e. R. ) -> ( -1R .R ( y .R w ) ) e. R. )
11 addclsr 
 |-  ( ( ( x .R z ) e. R. /\ ( -1R .R ( y .R w ) ) e. R. ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
12 6 10 11 syl2an 
 |-  ( ( ( x e. R. /\ z e. R. ) /\ ( y e. R. /\ w e. R. ) ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
13 12 an4s 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) e. R. )
14 mulclsr 
 |-  ( ( y e. R. /\ z e. R. ) -> ( y .R z ) e. R. )
15 mulclsr 
 |-  ( ( x e. R. /\ w e. R. ) -> ( x .R w ) e. R. )
16 addclsr 
 |-  ( ( ( y .R z ) e. R. /\ ( x .R w ) e. R. ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
17 14 15 16 syl2anr 
 |-  ( ( ( x e. R. /\ w e. R. ) /\ ( y e. R. /\ z e. R. ) ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
18 17 an42s 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( ( y .R z ) +R ( x .R w ) ) e. R. )
19 13 18 jca 
 |-  ( ( ( 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. ) )
20 mulclsr 
 |-  ( ( z e. R. /\ v e. R. ) -> ( z .R v ) e. R. )
21 mulclsr 
 |-  ( ( w e. R. /\ u e. R. ) -> ( w .R u ) e. R. )
22 mulclsr 
 |-  ( ( -1R e. R. /\ ( w .R u ) e. R. ) -> ( -1R .R ( w .R u ) ) e. R. )
23 7 21 22 sylancr 
 |-  ( ( w e. R. /\ u e. R. ) -> ( -1R .R ( w .R u ) ) e. R. )
24 addclsr 
 |-  ( ( ( z .R v ) e. R. /\ ( -1R .R ( w .R u ) ) e. R. ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. )
25 20 23 24 syl2an 
 |-  ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. )
26 25 an4s 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. )
27 mulclsr 
 |-  ( ( w e. R. /\ v e. R. ) -> ( w .R v ) e. R. )
28 mulclsr 
 |-  ( ( z e. R. /\ u e. R. ) -> ( z .R u ) e. R. )
29 addclsr 
 |-  ( ( ( w .R v ) e. R. /\ ( z .R u ) e. R. ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. )
30 27 28 29 syl2anr 
 |-  ( ( ( z e. R. /\ u e. R. ) /\ ( w e. R. /\ v e. R. ) ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. )
31 30 an42s 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. )
32 26 31 jca 
 |-  ( ( ( 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. ) )
33 ovex 
 |-  ( x .R ( z .R v ) ) e. _V
34 ovex 
 |-  ( x .R ( -1R .R ( w .R u ) ) ) e. _V
35 ovex 
 |-  ( -1R .R ( y .R ( w .R v ) ) ) e. _V
36 addcomsr 
 |-  ( f +R g ) = ( g +R f )
37 addasssr 
 |-  ( ( f +R g ) +R h ) = ( f +R ( g +R h ) )
38 ovex 
 |-  ( -1R .R ( y .R ( z .R u ) ) ) e. _V
39 33 34 35 36 37 38 caov42 
 |-  ( ( ( 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 ) ) ) ) )
40 distrsr 
 |-  ( x .R ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) ) = ( ( x .R ( z .R v ) ) +R ( x .R ( -1R .R ( w .R u ) ) ) )
41 distrsr 
 |-  ( y .R ( ( w .R v ) +R ( z .R u ) ) ) = ( ( y .R ( w .R v ) ) +R ( y .R ( z .R u ) ) )
42 41 oveq2i 
 |-  ( -1R .R ( y .R ( ( w .R v ) +R ( z .R u ) ) ) ) = ( -1R .R ( ( y .R ( w .R v ) ) +R ( y .R ( z .R u ) ) ) )
43 distrsr 
 |-  ( -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 ) ) ) )
44 42 43 eqtri 
 |-  ( -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 ) ) ) )
45 40 44 oveq12i 
 |-  ( ( 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 ) ) ) ) )
46 vex 
 |-  x e. _V
47 7 elexi 
 |-  -1R e. _V
48 vex 
 |-  z e. _V
49 mulcomsr 
 |-  ( f .R g ) = ( g .R f )
50 distrsr 
 |-  ( f .R ( g +R h ) ) = ( ( f .R g ) +R ( f .R h ) )
51 ovex 
 |-  ( y .R w ) e. _V
52 vex 
 |-  v e. _V
53 mulasssr 
 |-  ( ( f .R g ) .R h ) = ( f .R ( g .R h ) )
54 46 47 48 49 50 51 52 53 caovdilem 
 |-  ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) .R v ) = ( ( x .R ( z .R v ) ) +R ( -1R .R ( ( y .R w ) .R v ) ) )
55 mulasssr 
 |-  ( ( y .R w ) .R v ) = ( y .R ( w .R v ) )
56 55 oveq2i 
 |-  ( -1R .R ( ( y .R w ) .R v ) ) = ( -1R .R ( y .R ( w .R v ) ) )
57 56 oveq2i 
 |-  ( ( 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 ) ) ) )
58 54 57 eqtri 
 |-  ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) .R v ) = ( ( x .R ( z .R v ) ) +R ( -1R .R ( y .R ( w .R v ) ) ) )
59 vex 
 |-  y e. _V
60 vex 
 |-  w e. _V
61 vex 
 |-  u e. _V
62 59 46 48 49 50 60 61 53 caovdilem 
 |-  ( ( ( y .R z ) +R ( x .R w ) ) .R u ) = ( ( y .R ( z .R u ) ) +R ( x .R ( w .R u ) ) )
63 62 oveq2i 
 |-  ( -1R .R ( ( ( y .R z ) +R ( x .R w ) ) .R u ) ) = ( -1R .R ( ( y .R ( z .R u ) ) +R ( x .R ( w .R u ) ) ) )
64 distrsr 
 |-  ( -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 ) ) ) )
65 ovex 
 |-  ( w .R u ) e. _V
66 47 46 65 49 53 caov12 
 |-  ( -1R .R ( x .R ( w .R u ) ) ) = ( x .R ( -1R .R ( w .R u ) ) )
67 66 oveq2i 
 |-  ( ( -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 ) ) ) )
68 64 67 eqtri 
 |-  ( -1R .R ( ( y .R ( z .R u ) ) +R ( x .R ( w .R u ) ) ) ) = ( ( -1R .R ( y .R ( z .R u ) ) ) +R ( x .R ( -1R .R ( w .R u ) ) ) )
69 63 68 eqtri 
 |-  ( -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 ) ) ) )
70 58 69 oveq12i 
 |-  ( ( ( ( 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 ) ) ) ) )
71 39 45 70 3eqtr4ri 
 |-  ( ( ( ( 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 ) ) ) ) )
72 ovex 
 |-  ( y .R ( z .R v ) ) e. _V
73 ovex 
 |-  ( y .R ( -1R .R ( w .R u ) ) ) e. _V
74 ovex 
 |-  ( x .R ( w .R v ) ) e. _V
75 ovex 
 |-  ( x .R ( z .R u ) ) e. _V
76 72 73 74 36 37 75 caov42 
 |-  ( ( ( 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 ) ) ) ) )
77 distrsr 
 |-  ( y .R ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) ) = ( ( y .R ( z .R v ) ) +R ( y .R ( -1R .R ( w .R u ) ) ) )
78 distrsr 
 |-  ( x .R ( ( w .R v ) +R ( z .R u ) ) ) = ( ( x .R ( w .R v ) ) +R ( x .R ( z .R u ) ) )
79 77 78 oveq12i 
 |-  ( ( 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 ) ) ) )
80 59 46 48 49 50 60 52 53 caovdilem 
 |-  ( ( ( y .R z ) +R ( x .R w ) ) .R v ) = ( ( y .R ( z .R v ) ) +R ( x .R ( w .R v ) ) )
81 46 47 48 49 50 51 61 53 caovdilem 
 |-  ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) .R u ) = ( ( x .R ( z .R u ) ) +R ( -1R .R ( ( y .R w ) .R u ) ) )
82 mulasssr 
 |-  ( ( y .R w ) .R u ) = ( y .R ( w .R u ) )
83 82 oveq2i 
 |-  ( -1R .R ( ( y .R w ) .R u ) ) = ( -1R .R ( y .R ( w .R u ) ) )
84 47 59 65 49 53 caov12 
 |-  ( -1R .R ( y .R ( w .R u ) ) ) = ( y .R ( -1R .R ( w .R u ) ) )
85 83 84 eqtri 
 |-  ( -1R .R ( ( y .R w ) .R u ) ) = ( y .R ( -1R .R ( w .R u ) ) )
86 85 oveq2i 
 |-  ( ( 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 ) ) ) )
87 81 86 eqtri 
 |-  ( ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) .R u ) = ( ( x .R ( z .R u ) ) +R ( y .R ( -1R .R ( w .R u ) ) ) )
88 80 87 oveq12i 
 |-  ( ( ( ( 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 ) ) ) ) )
89 76 79 88 3eqtr4ri 
 |-  ( ( ( ( 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 ) ) ) )
90 1 2 3 4 5 19 32 71 89 ecovass 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )