Proof of Theorem tgfscgr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tglngval.p | . . 3
⊢ 𝑃 = (Base‘𝐺) | 
| 2 |  | lnxfr.d | . . 3
⊢  − =
(dist‘𝐺) | 
| 3 |  | tglngval.i | . . 3
⊢ 𝐼 = (Itv‘𝐺) | 
| 4 |  | tglngval.g | . . . 4
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 5 | 4 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐺 ∈ TarskiG) | 
| 6 |  | tglngval.x | . . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑃) | 
| 7 | 6 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑋 ∈ 𝑃) | 
| 8 |  | tglngval.y | . . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑃) | 
| 9 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ 𝑃) | 
| 10 |  | tgcolg.z | . . . 4
⊢ (𝜑 → 𝑍 ∈ 𝑃) | 
| 11 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑍 ∈ 𝑃) | 
| 12 |  | lnxfr.a | . . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 13 | 12 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐴 ∈ 𝑃) | 
| 14 |  | lnxfr.b | . . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 15 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐵 ∈ 𝑃) | 
| 16 |  | tgfscgr.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 17 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐶 ∈ 𝑃) | 
| 18 |  | tgfscgr.t | . . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑃) | 
| 19 | 18 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑇 ∈ 𝑃) | 
| 20 |  | tgfscgr.d | . . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 21 | 20 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐷 ∈ 𝑃) | 
| 22 |  | tgfscgr.5 | . . . 4
⊢ (𝜑 → 𝑋 ≠ 𝑌) | 
| 23 | 22 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑋 ≠ 𝑌) | 
| 24 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝑌 ∈ (𝑋𝐼𝑍)) | 
| 25 |  | lnxfr.r | . . . 4
⊢  ∼ =
(cgrG‘𝐺) | 
| 26 |  | tgfscgr.2 | . . . . 5
⊢ (𝜑 → 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝐶”〉) | 
| 27 | 26 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝐶”〉) | 
| 28 | 1, 2, 3, 25, 5, 7,
9, 11, 13, 15, 17, 27, 24 | tgbtwnxfr 28538 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → 𝐵 ∈ (𝐴𝐼𝐶)) | 
| 29 | 1, 2, 3, 25, 5, 7,
9, 11, 13, 15, 17, 27 | cgr3simp1 28528 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝑋 − 𝑌) = (𝐴 − 𝐵)) | 
| 30 | 1, 2, 3, 25, 5, 7,
9, 11, 13, 15, 17, 27 | cgr3simp2 28529 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝑌 − 𝑍) = (𝐵 − 𝐶)) | 
| 31 |  | tgfscgr.3 | . . . 4
⊢ (𝜑 → (𝑋 − 𝑇) = (𝐴 − 𝐷)) | 
| 32 | 31 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝑋 − 𝑇) = (𝐴 − 𝐷)) | 
| 33 |  | tgfscgr.4 | . . . 4
⊢ (𝜑 → (𝑌 − 𝑇) = (𝐵 − 𝐷)) | 
| 34 | 33 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝑌 − 𝑇) = (𝐵 − 𝐷)) | 
| 35 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 24, 28, 29, 30, 32, 34 | axtg5seg 28473 | . 2
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑋𝐼𝑍)) → (𝑍 − 𝑇) = (𝐶 − 𝐷)) | 
| 36 | 4 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐺 ∈ TarskiG) | 
| 37 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑌 ∈ 𝑃) | 
| 38 | 6 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑋 ∈ 𝑃) | 
| 39 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑍 ∈ 𝑃) | 
| 40 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐵 ∈ 𝑃) | 
| 41 | 12 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐴 ∈ 𝑃) | 
| 42 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐶 ∈ 𝑃) | 
| 43 | 18 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑇 ∈ 𝑃) | 
| 44 | 20 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐷 ∈ 𝑃) | 
| 45 | 22 | necomd 2996 | . . . 4
⊢ (𝜑 → 𝑌 ≠ 𝑋) | 
| 46 | 45 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑌 ≠ 𝑋) | 
| 47 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝑋 ∈ (𝑌𝐼𝑍)) | 
| 48 | 26 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝐶”〉) | 
| 49 | 1, 2, 3, 25, 36, 38, 37, 39, 41, 40, 42, 48 | cgr3swap12 28531 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 〈“𝑌𝑋𝑍”〉 ∼ 〈“𝐵𝐴𝐶”〉) | 
| 50 | 1, 2, 3, 25, 36, 37, 38, 39, 40, 41, 42, 49, 47 | tgbtwnxfr 28538 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → 𝐴 ∈ (𝐵𝐼𝐶)) | 
| 51 | 1, 2, 3, 25, 36, 37, 38, 39, 40, 41, 42, 49 | cgr3simp1 28528 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝑌 − 𝑋) = (𝐵 − 𝐴)) | 
| 52 | 1, 2, 3, 25, 36, 37, 38, 39, 40, 41, 42, 49 | cgr3simp2 28529 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝑋 − 𝑍) = (𝐴 − 𝐶)) | 
| 53 | 33 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝑌 − 𝑇) = (𝐵 − 𝐷)) | 
| 54 | 31 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝑋 − 𝑇) = (𝐴 − 𝐷)) | 
| 55 | 1, 2, 3, 36, 37, 38, 39, 40, 41, 42, 43, 44, 46, 47, 50, 51, 52, 53, 54 | axtg5seg 28473 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ (𝑌𝐼𝑍)) → (𝑍 − 𝑇) = (𝐶 − 𝐷)) | 
| 56 | 4 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐺 ∈ TarskiG) | 
| 57 | 6 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ 𝑃) | 
| 58 | 10 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑍 ∈ 𝑃) | 
| 59 | 8 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ 𝑃) | 
| 60 | 18 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑇 ∈ 𝑃) | 
| 61 | 12 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐴 ∈ 𝑃) | 
| 62 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ 𝑃) | 
| 63 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐵 ∈ 𝑃) | 
| 64 | 20 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐷 ∈ 𝑃) | 
| 65 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝑍 ∈ (𝑋𝐼𝑌)) | 
| 66 | 26 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 〈“𝑋𝑌𝑍”〉 ∼ 〈“𝐴𝐵𝐶”〉) | 
| 67 | 1, 2, 3, 25, 56, 57, 59, 58, 61, 63, 62, 66 | cgr3swap23 28532 | . . . 4
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 〈“𝑋𝑍𝑌”〉 ∼ 〈“𝐴𝐶𝐵”〉) | 
| 68 | 1, 2, 3, 25, 56, 57, 58, 59, 61, 62, 63, 67, 65 | tgbtwnxfr 28538 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ (𝐴𝐼𝐵)) | 
| 69 | 1, 2, 3, 25, 56, 57, 59, 58, 61, 63, 62, 66 | cgr3simp1 28528 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝑋 − 𝑌) = (𝐴 − 𝐵)) | 
| 70 | 1, 2, 3, 25, 56, 57, 58, 59, 61, 62, 63, 67 | cgr3simp2 28529 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝑍 − 𝑌) = (𝐶 − 𝐵)) | 
| 71 | 31 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝑋 − 𝑇) = (𝐴 − 𝐷)) | 
| 72 | 33 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝑌 − 𝑇) = (𝐵 − 𝐷)) | 
| 73 | 1, 2, 3, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 68, 69, 70, 71, 72 | tgifscgr 28516 | . 2
⊢ ((𝜑 ∧ 𝑍 ∈ (𝑋𝐼𝑌)) → (𝑍 − 𝑇) = (𝐶 − 𝐷)) | 
| 74 |  | tgfscgr.1 | . . 3
⊢ (𝜑 → (𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍)) | 
| 75 |  | tglngval.l | . . . 4
⊢ 𝐿 = (LineG‘𝐺) | 
| 76 | 1, 75, 3, 4, 6, 10,
8 | tgcolg 28562 | . . 3
⊢ (𝜑 → ((𝑌 ∈ (𝑋𝐿𝑍) ∨ 𝑋 = 𝑍) ↔ (𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑌𝐼𝑍) ∨ 𝑍 ∈ (𝑋𝐼𝑌)))) | 
| 77 | 74, 76 | mpbid 232 | . 2
⊢ (𝜑 → (𝑌 ∈ (𝑋𝐼𝑍) ∨ 𝑋 ∈ (𝑌𝐼𝑍) ∨ 𝑍 ∈ (𝑋𝐼𝑌))) | 
| 78 | 35, 55, 73, 77 | mpjao3dan 1434 | 1
⊢ (𝜑 → (𝑍 − 𝑇) = (𝐶 − 𝐷)) |