Proof of Theorem o2timesd
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | o2timesd.x | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐵) | 
| 2 |  | o2timesd.i | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) | 
| 3 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ( 1 · 𝑥) = ( 1 · 𝑋)) | 
| 4 |  | id 22 | . . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) | 
| 5 | 3, 4 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = 𝑋 → (( 1 · 𝑥) = 𝑥 ↔ ( 1 · 𝑋) = 𝑋)) | 
| 6 | 5 | rspcva 3620 | . . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) → ( 1 · 𝑋) = 𝑋) | 
| 7 | 6 | eqcomd 2743 | . . . 4
⊢ ((𝑋 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ( 1 · 𝑥) = 𝑥) → 𝑋 = ( 1 · 𝑋)) | 
| 8 | 1, 2, 7 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝑋 = ( 1 · 𝑋)) | 
| 9 | 8, 8 | oveq12d 7449 | . 2
⊢ (𝜑 → (𝑋 + 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋))) | 
| 10 |  | o2timesd.u | . . . 4
⊢ (𝜑 → 1 ∈ 𝐵) | 
| 11 | 10, 10, 1 | 3jca 1129 | . . 3
⊢ (𝜑 → ( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) | 
| 12 |  | o2timesd.e | . . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) | 
| 13 |  | oveq1 7438 | . . . . . 6
⊢ (𝑥 = 1 → (𝑥 + 𝑦) = ( 1 + 𝑦)) | 
| 14 | 13 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 1 → ((𝑥 + 𝑦) · 𝑧) = (( 1 + 𝑦) · 𝑧)) | 
| 15 |  | oveq1 7438 | . . . . . 6
⊢ (𝑥 = 1 → (𝑥 · 𝑧) = ( 1 · 𝑧)) | 
| 16 | 15 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 1 → ((𝑥 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + (𝑦 · 𝑧))) | 
| 17 | 14, 16 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 1 → (((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)))) | 
| 18 |  | oveq2 7439 | . . . . . 6
⊢ (𝑦 = 1 → ( 1 + 𝑦) = ( 1 + 1 )) | 
| 19 | 18 | oveq1d 7446 | . . . . 5
⊢ (𝑦 = 1 → (( 1 + 𝑦) · 𝑧) = (( 1 + 1 ) · 𝑧)) | 
| 20 |  | oveq1 7438 | . . . . . 6
⊢ (𝑦 = 1 → (𝑦 · 𝑧) = ( 1 · 𝑧)) | 
| 21 | 20 | oveq2d 7447 | . . . . 5
⊢ (𝑦 = 1 → (( 1 · 𝑧) + (𝑦 · 𝑧)) = (( 1 · 𝑧) + ( 1 · 𝑧))) | 
| 22 | 19, 21 | eqeq12d 2753 | . . . 4
⊢ (𝑦 = 1 → ((( 1 + 𝑦) · 𝑧) = (( 1 · 𝑧) + (𝑦 · 𝑧)) ↔ (( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)))) | 
| 23 |  | oveq2 7439 | . . . . 5
⊢ (𝑧 = 𝑋 → (( 1 + 1 ) · 𝑧) = (( 1 + 1 ) · 𝑋)) | 
| 24 |  | oveq2 7439 | . . . . . 6
⊢ (𝑧 = 𝑋 → ( 1 · 𝑧) = ( 1 · 𝑋)) | 
| 25 | 24, 24 | oveq12d 7449 | . . . . 5
⊢ (𝑧 = 𝑋 → (( 1 · 𝑧) + ( 1 · 𝑧)) = (( 1 · 𝑋) + ( 1 · 𝑋))) | 
| 26 | 23, 25 | eqeq12d 2753 | . . . 4
⊢ (𝑧 = 𝑋 → ((( 1 + 1 ) · 𝑧) = (( 1 · 𝑧) + ( 1 · 𝑧)) ↔ (( 1 + 1 ) · 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋)))) | 
| 27 | 17, 22, 26 | rspc3v 3638 | . . 3
⊢ (( 1 ∈ 𝐵 ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧)) → (( 1 + 1 ) · 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋)))) | 
| 28 | 11, 12, 27 | sylc 65 | . 2
⊢ (𝜑 → (( 1 + 1 ) · 𝑋) = (( 1 · 𝑋) + ( 1 · 𝑋))) | 
| 29 | 9, 28 | eqtr4d 2780 | 1
⊢ (𝜑 → (𝑋 + 𝑋) = (( 1 + 1 ) · 𝑋)) |