Proof of Theorem tgcgrextend
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tgcgrextend.4 | . . . 4
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | 
| 3 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) | 
| 4 | 3 | oveq1d 7446 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴 − 𝐶) = (𝐵 − 𝐶)) | 
| 5 |  | tkgeom.p | . . . . 5
⊢ 𝑃 = (Base‘𝐺) | 
| 6 |  | tkgeom.d | . . . . 5
⊢  − =
(dist‘𝐺) | 
| 7 |  | tkgeom.i | . . . . 5
⊢ 𝐼 = (Itv‘𝐺) | 
| 8 |  | tkgeom.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 9 | 8 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐺 ∈ TarskiG) | 
| 10 |  | tgcgrextend.a | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 11 | 10 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐴 ∈ 𝑃) | 
| 12 |  | tgcgrextend.b | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 13 | 12 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐵 ∈ 𝑃) | 
| 14 |  | tgcgrextend.d | . . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 15 | 14 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐷 ∈ 𝑃) | 
| 16 |  | tgcgrextend.e | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) | 
| 17 | 16 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐸 ∈ 𝑃) | 
| 18 |  | tgcgrextend.3 | . . . . . 6
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 19 | 18 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 20 | 5, 6, 7, 9, 11, 13, 15, 17, 19, 3 | tgcgreq 28490 | . . . 4
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐷 = 𝐸) | 
| 21 | 20 | oveq1d 7446 | . . 3
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐷 − 𝐹) = (𝐸 − 𝐹)) | 
| 22 | 2, 4, 21 | 3eqtr4d 2787 | . 2
⊢ ((𝜑 ∧ 𝐴 = 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | 
| 23 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ TarskiG) | 
| 24 |  | tgcgrextend.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 25 | 24 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐶 ∈ 𝑃) | 
| 26 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑃) | 
| 27 |  | tgcgrextend.f | . . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) | 
| 28 | 27 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐹 ∈ 𝑃) | 
| 29 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐷 ∈ 𝑃) | 
| 30 | 12 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑃) | 
| 31 | 16 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐸 ∈ 𝑃) | 
| 32 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) | 
| 33 |  | tgcgrextend.1 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) | 
| 34 | 33 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ (𝐴𝐼𝐶)) | 
| 35 |  | tgcgrextend.2 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐼𝐹)) | 
| 36 | 35 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝐸 ∈ (𝐷𝐼𝐹)) | 
| 37 | 18 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 38 | 1 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | 
| 39 | 5, 6, 7, 23, 26, 29 | tgcgrtriv 28492 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 − 𝐴) = (𝐷 − 𝐷)) | 
| 40 | 5, 6, 7, 23, 26, 30, 29, 31, 37 | tgcgrcomlr 28488 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) | 
| 41 | 5, 6, 7, 23, 26, 30, 25, 29, 31, 28, 26, 29, 32, 34, 36, 37, 38, 39, 40 | axtg5seg 28473 | . . 3
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐶 − 𝐴) = (𝐹 − 𝐷)) | 
| 42 | 5, 6, 7, 23, 25, 26, 28, 29, 41 | tgcgrcomlr 28488 | . 2
⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → (𝐴 − 𝐶) = (𝐷 − 𝐹)) | 
| 43 | 22, 42 | pm2.61dane 3029 | 1
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐷 − 𝐹)) |