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