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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 ·e 𝐵 ) ·e 𝐶 ) = ( 𝐴 ·e ( 𝐵 ·e 𝐶 ) ) )

Proof

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