Metamath Proof Explorer

Theorem xmulass

Description: Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass which has to avoid the "undefined" combinations +oo +e -oo and -oo +e +oo . The equivalent "undefined" expression here would be 0 *e +oo , but since this is defined to equal 0 any zeroes in the expression make the whole thing evaluate to zero (on both sides), thus establishing the identity in this case. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmulass 
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = A -> ( x *e B ) = ( A *e B ) )
2 1 oveq1d 
 |-  ( x = A -> ( ( x *e B ) *e C ) = ( ( A *e B ) *e C ) )
3 oveq1 
 |-  ( x = A -> ( x *e ( B *e C ) ) = ( A *e ( B *e C ) ) )
4 2 3 eqeq12d 
 |-  ( x = A -> ( ( ( x *e B ) *e C ) = ( x *e ( B *e C ) ) <-> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) ) )
5 oveq1 
 |-  ( x = -e A -> ( x *e B ) = ( -e A *e B ) )
6 5 oveq1d 
 |-  ( x = -e A -> ( ( x *e B ) *e C ) = ( ( -e A *e B ) *e C ) )
7 oveq1 
 |-  ( x = -e A -> ( x *e ( B *e C ) ) = ( -e A *e ( B *e C ) ) )
8 6 7 eqeq12d 
 |-  ( x = -e A -> ( ( ( x *e B ) *e C ) = ( x *e ( B *e C ) ) <-> ( ( -e A *e B ) *e C ) = ( -e A *e ( B *e C ) ) ) )
9 xmulcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A *e B ) e. RR* )
10 xmulcl 
 |-  ( ( ( A *e B ) e. RR* /\ C e. RR* ) -> ( ( A *e B ) *e C ) e. RR* )
11 9 10 stoic3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A *e B ) *e C ) e. RR* )
12 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> A e. RR* )
13 xmulcl 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( B *e C ) e. RR* )
14 13 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( B *e C ) e. RR* )
15 xmulcl 
 |-  ( ( A e. RR* /\ ( B *e C ) e. RR* ) -> ( A *e ( B *e C ) ) e. RR* )
16 12 14 15 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A *e ( B *e C ) ) e. RR* )
17 oveq2 
 |-  ( y = B -> ( x *e y ) = ( x *e B ) )
18 17 oveq1d 
 |-  ( y = B -> ( ( x *e y ) *e C ) = ( ( x *e B ) *e C ) )
19 oveq1 
 |-  ( y = B -> ( y *e C ) = ( B *e C ) )
20 19 oveq2d 
 |-  ( y = B -> ( x *e ( y *e C ) ) = ( x *e ( B *e C ) ) )
21 18 20 eqeq12d 
 |-  ( y = B -> ( ( ( x *e y ) *e C ) = ( x *e ( y *e C ) ) <-> ( ( x *e B ) *e C ) = ( x *e ( B *e C ) ) ) )
22 oveq2 
 |-  ( y = -e B -> ( x *e y ) = ( x *e -e B ) )
23 22 oveq1d 
 |-  ( y = -e B -> ( ( x *e y ) *e C ) = ( ( x *e -e B ) *e C ) )
24 oveq1 
 |-  ( y = -e B -> ( y *e C ) = ( -e B *e C ) )
25 24 oveq2d 
 |-  ( y = -e B -> ( x *e ( y *e C ) ) = ( x *e ( -e B *e C ) ) )
26 23 25 eqeq12d 
 |-  ( y = -e B -> ( ( ( x *e y ) *e C ) = ( x *e ( y *e C ) ) <-> ( ( x *e -e B ) *e C ) = ( x *e ( -e B *e C ) ) ) )
27 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> x e. RR* )
28 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> B e. RR* )
29 xmulcl 
 |-  ( ( x e. RR* /\ B e. RR* ) -> ( x *e B ) e. RR* )
30 27 28 29 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e B ) e. RR* )
31 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> C e. RR* )
32 xmulcl 
 |-  ( ( ( x *e B ) e. RR* /\ C e. RR* ) -> ( ( x *e B ) *e C ) e. RR* )
33 30 31 32 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( ( x *e B ) *e C ) e. RR* )
34 14 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( B *e C ) e. RR* )
35 xmulcl 
 |-  ( ( x e. RR* /\ ( B *e C ) e. RR* ) -> ( x *e ( B *e C ) ) e. RR* )
36 27 34 35 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e ( B *e C ) ) e. RR* )
37 oveq2 
 |-  ( z = C -> ( ( x *e y ) *e z ) = ( ( x *e y ) *e C ) )
38 oveq2 
 |-  ( z = C -> ( y *e z ) = ( y *e C ) )
39 38 oveq2d 
 |-  ( z = C -> ( x *e ( y *e z ) ) = ( x *e ( y *e C ) ) )
40 37 39 eqeq12d 
 |-  ( z = C -> ( ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) <-> ( ( x *e y ) *e C ) = ( x *e ( y *e C ) ) ) )
41 oveq2 
 |-  ( z = -e C -> ( ( x *e y ) *e z ) = ( ( x *e y ) *e -e C ) )
42 oveq2 
 |-  ( z = -e C -> ( y *e z ) = ( y *e -e C ) )
43 42 oveq2d 
 |-  ( z = -e C -> ( x *e ( y *e z ) ) = ( x *e ( y *e -e C ) ) )
44 41 43 eqeq12d 
 |-  ( z = -e C -> ( ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) <-> ( ( x *e y ) *e -e C ) = ( x *e ( y *e -e C ) ) ) )
45 27 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> x e. RR* )
46 simprl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> y e. RR* )
47 xmulcl 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x *e y ) e. RR* )
48 45 46 47 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e y ) e. RR* )
49 31 adantr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> C e. RR* )
50 xmulcl 
 |-  ( ( ( x *e y ) e. RR* /\ C e. RR* ) -> ( ( x *e y ) *e C ) e. RR* )
51 48 49 50 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( ( x *e y ) *e C ) e. RR* )
52 xmulcl 
 |-  ( ( y e. RR* /\ C e. RR* ) -> ( y *e C ) e. RR* )
53 46 49 52 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( y *e C ) e. RR* )
54 xmulcl 
 |-  ( ( x e. RR* /\ ( y *e C ) e. RR* ) -> ( x *e ( y *e C ) ) e. RR* )
55 45 53 54 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e ( y *e C ) ) e. RR* )
56 xmulasslem3 
 |-  ( ( ( x e. RR* /\ 0 < x ) /\ ( y e. RR* /\ 0 < y ) /\ ( z e. RR* /\ 0 < z ) ) -> ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) )
57 56 ad4ant234 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) /\ ( z e. RR* /\ 0 < z ) ) -> ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) )
58 xmul01 
 |-  ( ( x *e y ) e. RR* -> ( ( x *e y ) *e 0 ) = 0 )
59 48 58 syl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( ( x *e y ) *e 0 ) = 0 )
60 xmul01 
 |-  ( x e. RR* -> ( x *e 0 ) = 0 )
61 45 60 syl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e 0 ) = 0 )
62 59 61 eqtr4d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( ( x *e y ) *e 0 ) = ( x *e 0 ) )
63 xmul01 
 |-  ( y e. RR* -> ( y *e 0 ) = 0 )
64 63 ad2antrl 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( y *e 0 ) = 0 )
65 64 oveq2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e ( y *e 0 ) ) = ( x *e 0 ) )
66 62 65 eqtr4d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( ( x *e y ) *e 0 ) = ( x *e ( y *e 0 ) ) )
67 oveq2 
 |-  ( z = 0 -> ( ( x *e y ) *e z ) = ( ( x *e y ) *e 0 ) )
68 oveq2 
 |-  ( z = 0 -> ( y *e z ) = ( y *e 0 ) )
69 68 oveq2d 
 |-  ( z = 0 -> ( x *e ( y *e z ) ) = ( x *e ( y *e 0 ) ) )
70 67 69 eqeq12d 
 |-  ( z = 0 -> ( ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) <-> ( ( x *e y ) *e 0 ) = ( x *e ( y *e 0 ) ) ) )
71 66 70 syl5ibrcom 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( z = 0 -> ( ( x *e y ) *e z ) = ( x *e ( y *e z ) ) ) )
72 xmulneg2 
 |-  ( ( ( x *e y ) e. RR* /\ C e. RR* ) -> ( ( x *e y ) *e -e C ) = -e ( ( x *e y ) *e C ) )
73 48 49 72 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( ( x *e y ) *e -e C ) = -e ( ( x *e y ) *e C ) )
74 xmulneg2 
 |-  ( ( y e. RR* /\ C e. RR* ) -> ( y *e -e C ) = -e ( y *e C ) )
75 46 49 74 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( y *e -e C ) = -e ( y *e C ) )
76 75 oveq2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e ( y *e -e C ) ) = ( x *e -e ( y *e C ) ) )
77 xmulneg2 
 |-  ( ( x e. RR* /\ ( y *e C ) e. RR* ) -> ( x *e -e ( y *e C ) ) = -e ( x *e ( y *e C ) ) )
78 45 53 77 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e -e ( y *e C ) ) = -e ( x *e ( y *e C ) ) )
79 76 78 eqtrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( x *e ( y *e -e C ) ) = -e ( x *e ( y *e C ) ) )
80 40 44 51 55 49 57 71 73 79 xmulasslem 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) /\ ( y e. RR* /\ 0 < y ) ) -> ( ( x *e y ) *e C ) = ( x *e ( y *e C ) ) )
81 xmul02 
 |-  ( C e. RR* -> ( 0 *e C ) = 0 )
82 81 3ad2ant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( 0 *e C ) = 0 )
83 82 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( 0 *e C ) = 0 )
84 60 ad2antrl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e 0 ) = 0 )
85 83 84 eqtr4d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( 0 *e C ) = ( x *e 0 ) )
86 84 oveq1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( ( x *e 0 ) *e C ) = ( 0 *e C ) )
87 83 oveq2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e ( 0 *e C ) ) = ( x *e 0 ) )
88 85 86 87 3eqtr4d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( ( x *e 0 ) *e C ) = ( x *e ( 0 *e C ) ) )
89 oveq2 
 |-  ( y = 0 -> ( x *e y ) = ( x *e 0 ) )
90 89 oveq1d 
 |-  ( y = 0 -> ( ( x *e y ) *e C ) = ( ( x *e 0 ) *e C ) )
91 oveq1 
 |-  ( y = 0 -> ( y *e C ) = ( 0 *e C ) )
92 91 oveq2d 
 |-  ( y = 0 -> ( x *e ( y *e C ) ) = ( x *e ( 0 *e C ) ) )
93 90 92 eqeq12d 
 |-  ( y = 0 -> ( ( ( x *e y ) *e C ) = ( x *e ( y *e C ) ) <-> ( ( x *e 0 ) *e C ) = ( x *e ( 0 *e C ) ) ) )
94 88 93 syl5ibrcom 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( y = 0 -> ( ( x *e y ) *e C ) = ( x *e ( y *e C ) ) ) )
95 xmulneg2 
 |-  ( ( x e. RR* /\ B e. RR* ) -> ( x *e -e B ) = -e ( x *e B ) )
96 27 28 95 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e -e B ) = -e ( x *e B ) )
97 96 oveq1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( ( x *e -e B ) *e C ) = ( -e ( x *e B ) *e C ) )
98 xmulneg1 
 |-  ( ( ( x *e B ) e. RR* /\ C e. RR* ) -> ( -e ( x *e B ) *e C ) = -e ( ( x *e B ) *e C ) )
99 30 31 98 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( -e ( x *e B ) *e C ) = -e ( ( x *e B ) *e C ) )
100 97 99 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( ( x *e -e B ) *e C ) = -e ( ( x *e B ) *e C ) )
101 xmulneg1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( -e B *e C ) = -e ( B *e C ) )
102 28 31 101 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( -e B *e C ) = -e ( B *e C ) )
103 102 oveq2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e ( -e B *e C ) ) = ( x *e -e ( B *e C ) ) )
104 xmulneg2 
 |-  ( ( x e. RR* /\ ( B *e C ) e. RR* ) -> ( x *e -e ( B *e C ) ) = -e ( x *e ( B *e C ) ) )
105 27 34 104 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e -e ( B *e C ) ) = -e ( x *e ( B *e C ) ) )
106 103 105 eqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( x *e ( -e B *e C ) ) = -e ( x *e ( B *e C ) ) )
107 21 26 33 36 28 80 94 100 106 xmulasslem 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. RR* /\ 0 < x ) ) -> ( ( x *e B ) *e C ) = ( x *e ( B *e C ) ) )
108 xmul02 
 |-  ( B e. RR* -> ( 0 *e B ) = 0 )
109 108 3ad2ant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( 0 *e B ) = 0 )
110 109 oveq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( 0 *e B ) *e C ) = ( 0 *e C ) )
111 xmul02 
 |-  ( ( B *e C ) e. RR* -> ( 0 *e ( B *e C ) ) = 0 )
112 14 111 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( 0 *e ( B *e C ) ) = 0 )
113 82 110 112 3eqtr4d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( 0 *e B ) *e C ) = ( 0 *e ( B *e C ) ) )
114 oveq1 
 |-  ( x = 0 -> ( x *e B ) = ( 0 *e B ) )
115 114 oveq1d 
 |-  ( x = 0 -> ( ( x *e B ) *e C ) = ( ( 0 *e B ) *e C ) )
116 oveq1 
 |-  ( x = 0 -> ( x *e ( B *e C ) ) = ( 0 *e ( B *e C ) ) )
117 115 116 eqeq12d 
 |-  ( x = 0 -> ( ( ( x *e B ) *e C ) = ( x *e ( B *e C ) ) <-> ( ( 0 *e B ) *e C ) = ( 0 *e ( B *e C ) ) ) )
118 113 117 syl5ibrcom 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x = 0 -> ( ( x *e B ) *e C ) = ( x *e ( B *e C ) ) ) )
119 xmulneg1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -e A *e B ) = -e ( A *e B ) )
120 119 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -e A *e B ) = -e ( A *e B ) )
121 120 oveq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( -e A *e B ) *e C ) = ( -e ( A *e B ) *e C ) )
122 xmulneg1 
 |-  ( ( ( A *e B ) e. RR* /\ C e. RR* ) -> ( -e ( A *e B ) *e C ) = -e ( ( A *e B ) *e C ) )
123 9 122 stoic3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -e ( A *e B ) *e C ) = -e ( ( A *e B ) *e C ) )
124 121 123 eqtrd 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( -e A *e B ) *e C ) = -e ( ( A *e B ) *e C ) )
125 xmulneg1 
 |-  ( ( A e. RR* /\ ( B *e C ) e. RR* ) -> ( -e A *e ( B *e C ) ) = -e ( A *e ( B *e C ) ) )
126 12 14 125 syl2anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( -e A *e ( B *e C ) ) = -e ( A *e ( B *e C ) ) )
127 4 8 11 16 12 107 118 124 126 xmulasslem 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A *e B ) *e C ) = ( A *e ( B *e C ) ) )