Proof of Theorem o2timesd
Step | Hyp | Ref
| Expression |
1 | | o2timesd.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | o2timesd.i |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) |
3 | | oveq2 7420 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → ( 1 · 𝑥) = ( 1 · 𝑋)) |
4 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
5 | 3, 4 | eqeq12d 2747 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · 𝑋) = 𝑋)) |
6 | 5 | rspcva 3610 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) → ( 1 · 𝑋) = 𝑋) |
7 | 6 | eqcomd 2737 |
. . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) → 𝑋 = ( 1 · 𝑋)) |
8 | 1, 2, 7 | syl2anc 583 |
. . 3
⊢ (𝜑 → 𝑋 = ( 1 · 𝑋)) |
9 | 8, 8 | oveq12d 7430 |
. 2
⊢ (𝜑 → (𝑋 + 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋))) |
10 | | o2timesd.u |
. . . 4
⊢ (𝜑 → 1 ∈ 𝐵) |
11 | 10, 10, 1 | 3jca 1127 |
. . 3
⊢ (𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) |
12 | | o2timesd.e |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
13 | | oveq1 7419 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑥 + 𝑦) = ( 1 + 𝑦)) |
14 | 13 | oveq1d 7427 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑥 + 𝑦) · 𝑧) = (( 1 + 𝑦) · 𝑧)) |
15 | | oveq1 7419 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑥 · 𝑧) = ( 1 · 𝑧)) |
16 | 15 | oveq1d 7427 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + (𝑦 · 𝑧))) |
17 | 14, 16 | eqeq12d 2747 |
. . . 4
⊢ (𝑥 = 1 → (((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)))) |
18 | | oveq2 7420 |
. . . . . 6
⊢ (𝑦 = 1 → ( 1 + 𝑦) = ( 1 + 1 )) |
19 | 18 | oveq1d 7427 |
. . . . 5
⊢ (𝑦 = 1 → (( 1 + 𝑦) · 𝑧) = (( 1 + 1 ) · 𝑧)) |
20 | | oveq1 7419 |
. . . . . 6
⊢ (𝑦 = 1 → (𝑦 · 𝑧) = ( 1 · 𝑧)) |
21 | 20 | oveq2d 7428 |
. . . . 5
⊢ (𝑦 = 1 → (( 1 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + ( 1 · 𝑧))) |
22 | 19, 21 | eqeq12d 2747 |
. . . 4
⊢ (𝑦 = 1 → ((( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)))) |
23 | | oveq2 7420 |
. . . . 5
⊢ (𝑧 = 𝑋 → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · 𝑋)) |
24 | | oveq2 7420 |
. . . . . 6
⊢ (𝑧 = 𝑋 → ( 1 · 𝑧) = ( 1 · 𝑋)) |
25 | 24, 24 | oveq12d 7430 |
. . . . 5
⊢ (𝑧 = 𝑋 → (( 1 · 𝑧) + ( 1 · 𝑧)) = (( 1 · 𝑋) + ( 1 · 𝑋))) |
26 | 23, 25 | eqeq12d 2747 |
. . . 4
⊢ (𝑧 = 𝑋 → ((( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)) ↔ (( 1 + 1 ) · 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋)))) |
27 | 17, 22, 26 | rspc3v 3627 |
. . 3
⊢ (( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → (( 1 + 1 ) · 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋)))) |
28 | 11, 12, 27 | sylc 65 |
. 2
⊢ (𝜑 → (( 1 + 1 ) · 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋))) |
29 | 9, 28 | eqtr4d 2774 |
1
⊢ (𝜑 → (𝑋 + 𝑋) = (( 1 + 1 ) · 𝑋)) |