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 ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 B ⋅ 𝑒 C

Proof

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