Theorem xmulass 11362

Description: Associativity of the extended real multiplication operation. Surprisingly, there are no restrictions on the values, unlike xaddass 11324 which has to avoid the "undefined" combinations +oo +e -oo and -oo +e +oo. The equivalent "undefined" expression here would be 0 xe +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.)

Assertion

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

Proof of Theorem xmulass

Dummy variables x y z are mutually distinct and distinct from all other variables.

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

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   class class class wbr 4401  (class class class)co 6201   0cc0 9394   RR*cxr 9529   < clt 9530   -ecxne 11198   xecxmu 11200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-cnex 9450  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470  ax-pre-mulgt0 9471

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-iun 4282  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-po 4750  df-so 4751  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-1st 6688  df-2nd 6689  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-xr 9534  df-ltxr 9535  df-le 9536  df-sub 9709  df-neg 9710  df-xneg 11201  df-xmul 11203

This theorem is referenced by:  xlemul1  11365  xrsmcmn  17965  nmoi2  20442  xmulcand  26242  xreceu  26243  xdivrec  26248  xrge0slmod  26458