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