| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simprr 772 | . . 3
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐸 − 𝑓) = (𝐵 − 𝐶)) | 
| 2 |  | tgsas.p | . . . . 5
⊢ 𝑃 = (Base‘𝐺) | 
| 3 |  | tgsas.i | . . . . 5
⊢ 𝐼 = (Itv‘𝐺) | 
| 4 |  | tgasa.l | . . . . 5
⊢ 𝐿 = (LineG‘𝐺) | 
| 5 |  | tgsas.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 6 | 5 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐺 ∈ TarskiG) | 
| 7 |  | tgsas.f | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑃) | 
| 8 | 7 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ 𝑃) | 
| 9 |  | tgsas.d | . . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 10 | 9 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ∈ 𝑃) | 
| 11 |  | tgsas.e | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) | 
| 12 | 11 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸 ∈ 𝑃) | 
| 13 |  | tgsas.m | . . . . . . 7
⊢  − =
(dist‘𝐺) | 
| 14 |  | tgsas.a | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 15 |  | tgsas.b | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 16 |  | tgsas.c | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 17 |  | tgasa.3 | . . . . . . 7
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | 
| 18 |  | tgasa.1 | . . . . . . 7
⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 19 | 2, 3, 13, 5, 14, 15, 16, 9, 11, 7, 17, 4, 18 | cgrancol 28838 | . . . . . 6
⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 20 | 19 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 21 |  | eqid 2736 | . . . . . 6
⊢
(hlG‘𝐺) =
(hlG‘𝐺) | 
| 22 |  | simplr 768 | . . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ 𝑃) | 
| 23 | 16 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐶 ∈ 𝑃) | 
| 24 | 14 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐴 ∈ 𝑃) | 
| 25 | 15 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐵 ∈ 𝑃) | 
| 26 | 18 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 27 | 5 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐺 ∈ TarskiG) | 
| 28 | 9 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐷 ∈ 𝑃) | 
| 29 | 11 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐸 ∈ 𝑃) | 
| 30 | 7 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐹 ∈ 𝑃) | 
| 31 | 14 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐴 ∈ 𝑃) | 
| 32 | 15 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐵 ∈ 𝑃) | 
| 33 | 16 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 𝐶 ∈ 𝑃) | 
| 34 | 2, 3, 5, 21, 14, 15, 16, 9, 11, 7, 17 | cgracom 28831 | . . . . . . . . . 10
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) | 
| 35 | 34 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) | 
| 36 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) | 
| 37 | 2, 4, 3, 27, 28, 30, 29, 36 | colcom 28567 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐸 ∈ (𝐹𝐿𝐷) ∨ 𝐹 = 𝐷)) | 
| 38 | 2, 4, 3, 27, 30, 28, 29, 37 | colrot1 28568 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 39 | 2, 3, 13, 27, 28, 29, 30, 31, 32, 33, 35, 4, 38 | cgracol 28837 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 40 | 18 | ad3antrrr 730 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) ∧ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 41 | 39, 40 | pm2.65da 816 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ (𝐸 ∈ (𝐷𝐿𝐹) ∨ 𝐷 = 𝐹)) | 
| 42 |  | eqid 2736 | . . . . . . . . . 10
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) | 
| 43 | 17 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) | 
| 44 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hlG‘𝐺)‘𝐸)𝐹) | 
| 45 | 2, 3, 21, 6, 24, 25, 23, 10, 12, 8, 43, 22, 44 | cgrahl2 28826 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑓”〉) | 
| 46 | 2, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17 | cgrane1 28821 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| 47 | 2, 3, 21, 14, 14, 15, 5, 46 | hlid 28618 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴((hlG‘𝐺)‘𝐵)𝐴) | 
| 48 | 47 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐴((hlG‘𝐺)‘𝐵)𝐴) | 
| 49 | 2, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17 | cgrane2 28822 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ 𝐶) | 
| 50 | 49 | necomd 2995 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ≠ 𝐵) | 
| 51 | 2, 3, 21, 16, 14, 15, 5, 50 | hlid 28618 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶((hlG‘𝐺)‘𝐵)𝐶) | 
| 52 | 51 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐶((hlG‘𝐺)‘𝐵)𝐶) | 
| 53 |  | tgasa.2 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 54 | 2, 13, 3, 5, 14, 15, 9, 11, 53 | tgcgrcomlr 28489 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 − 𝐴) = (𝐸 − 𝐷)) | 
| 55 | 54 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐴) = (𝐸 − 𝐷)) | 
| 56 | 1 | eqcomd 2742 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐶) = (𝐸 − 𝑓)) | 
| 57 | 2, 3, 21, 6, 24, 25, 23, 10, 12, 22, 45, 24, 13, 23, 48, 52, 55, 56 | cgracgr 28827 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐴 − 𝐶) = (𝐷 − 𝑓)) | 
| 58 | 2, 13, 3, 6, 24, 23, 10, 22, 57 | tgcgrcomlr 28489 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐶 − 𝐴) = (𝑓 − 𝐷)) | 
| 59 | 53 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 60 | 2, 13, 42, 6, 23, 24, 25, 22, 10, 12, 58, 59, 56 | trgcgr 28525 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrG‘𝐺)〈“𝑓𝐷𝐸”〉) | 
| 61 | 2, 3, 4, 5, 16, 14, 15, 18 | ncolne1 28634 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ≠ 𝐴) | 
| 62 | 61 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐶 ≠ 𝐴) | 
| 63 | 2, 13, 3, 6, 23, 24, 22, 10, 58, 62 | tgcgrneq 28492 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ≠ 𝐷) | 
| 64 | 2, 3, 21, 22, 8, 10, 6, 63 | hlid 28618 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hlG‘𝐺)‘𝐷)𝑓) | 
| 65 |  | tgasa.4 | . . . . . . . . . . . . 13
⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐹𝐷𝐸”〉) | 
| 66 | 2, 3, 21, 5, 16, 14, 15, 7, 9, 11, 65 | cgrane4 28824 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ≠ 𝐸) | 
| 67 | 66 | necomd 2995 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ≠ 𝐷) | 
| 68 | 2, 3, 21, 11, 14, 9, 5, 67 | hlid 28618 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸((hlG‘𝐺)‘𝐷)𝐸) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸((hlG‘𝐺)‘𝐷)𝐸) | 
| 70 | 2, 3, 21, 6, 23, 24, 25, 22, 10, 12, 22, 12, 60, 64, 69 | iscgrad 28820 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝑓𝐷𝐸”〉) | 
| 71 | 66 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐷 ≠ 𝐸) | 
| 72 | 2, 3, 6, 21, 22, 10, 12, 63, 71 | cgraswap 28829 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝑓𝐷𝐸”〉(cgrA‘𝐺)〈“𝐸𝐷𝑓”〉) | 
| 73 | 2, 3, 6, 21, 23, 24, 25, 22, 10, 12, 70, 12, 10, 22, 72 | cgratr 28832 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐸𝐷𝑓”〉) | 
| 74 | 2, 3, 21, 5, 16, 14, 15, 7, 9, 11, 65 | cgrane3 28823 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ≠ 𝐹) | 
| 75 | 74 | necomd 2995 | . . . . . . . . . 10
⊢ (𝜑 → 𝐹 ≠ 𝐷) | 
| 76 | 2, 3, 5, 21, 7, 9,
11, 75, 66 | cgraswap 28829 | . . . . . . . . 9
⊢ (𝜑 → 〈“𝐹𝐷𝐸”〉(cgrA‘𝐺)〈“𝐸𝐷𝐹”〉) | 
| 77 | 2, 3, 5, 21, 16, 14, 15, 7, 9, 11, 65, 11, 9, 7, 76 | cgratr 28832 | . . . . . . . 8
⊢ (𝜑 → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐸𝐷𝐹”〉) | 
| 78 | 77 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 〈“𝐶𝐴𝐵”〉(cgrA‘𝐺)〈“𝐸𝐷𝐹”〉) | 
| 79 | 2, 3, 4, 5, 11, 9,
67 | tgelrnln 28639 | . . . . . . . . 9
⊢ (𝜑 → (𝐸𝐿𝐷) ∈ ran 𝐿) | 
| 80 | 79 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐸𝐿𝐷) ∈ ran 𝐿) | 
| 81 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑎 = 𝑢) | 
| 82 | 81 | eleq1d 2825 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ↔ 𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)))) | 
| 83 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → 𝑏 = 𝑣) | 
| 84 | 83 | eleq1d 2825 | . . . . . . . . . . 11
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ↔ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷)))) | 
| 85 | 82, 84 | anbi12d 632 | . . . . . . . . . 10
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → ((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ↔ (𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))))) | 
| 86 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑡 = 𝑤) | 
| 87 |  | simpll 766 | . . . . . . . . . . . . 13
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑎 = 𝑢) | 
| 88 |  | simplr 768 | . . . . . . . . . . . . 13
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → 𝑏 = 𝑣) | 
| 89 | 87, 88 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → (𝑎𝐼𝑏) = (𝑢𝐼𝑣)) | 
| 90 | 86, 89 | eleq12d 2834 | . . . . . . . . . . 11
⊢ (((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) ∧ 𝑡 = 𝑤) → (𝑡 ∈ (𝑎𝐼𝑏) ↔ 𝑤 ∈ (𝑢𝐼𝑣))) | 
| 91 | 90 | cbvrexdva 3239 | . . . . . . . . . 10
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏) ↔ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣))) | 
| 92 | 85, 91 | anbi12d 632 | . . . . . . . . 9
⊢ ((𝑎 = 𝑢 ∧ 𝑏 = 𝑣) → (((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏)) ↔ ((𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣)))) | 
| 93 | 92 | cbvopabv 5215 | . . . . . . . 8
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑏 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑡 ∈ (𝐸𝐿𝐷)𝑡 ∈ (𝑎𝐼𝑏))} = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝑃 ∖ (𝐸𝐿𝐷)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐸𝐿𝐷))) ∧ ∃𝑤 ∈ (𝐸𝐿𝐷)𝑤 ∈ (𝑢𝐼𝑣))} | 
| 94 | 2, 3, 4, 5, 11, 9,
67 | tglinerflx1 28642 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ (𝐸𝐿𝐷)) | 
| 95 | 94 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸 ∈ (𝐸𝐿𝐷)) | 
| 96 | 2, 4, 3, 5, 9, 11,
7, 19 | ncolcom 28570 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐹 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 97 |  | pm2.45 881 | . . . . . . . . . . 11
⊢ (¬
(𝐹 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷) → ¬ 𝐹 ∈ (𝐸𝐿𝐷)) | 
| 98 | 96, 97 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐹 ∈ (𝐸𝐿𝐷)) | 
| 99 | 98 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → ¬ 𝐹 ∈ (𝐸𝐿𝐷)) | 
| 100 | 2, 3, 21, 22, 8, 12, 6, 44 | hlcomd 28613 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹((hlG‘𝐺)‘𝐸)𝑓) | 
| 101 | 2, 3, 4, 6, 80, 12, 93, 21, 95, 8, 22, 99, 100 | hphl 28780 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝑓) | 
| 102 | 2, 3, 4, 6, 80, 8,
93, 22, 101 | hpgcom 28776 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹) | 
| 103 | 2, 3, 4, 5, 79, 7,
93, 98 | hpgid 28775 | . . . . . . . 8
⊢ (𝜑 → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹) | 
| 104 | 103 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹((hpG‘𝐺)‘(𝐸𝐿𝐷))𝐹) | 
| 105 | 2, 3, 13, 6, 23, 24, 25, 12, 10, 8, 4, 26, 41, 22, 8, 21, 73, 78, 102, 104 | acopyeu 28843 | . . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓((hlG‘𝐺)‘𝐷)𝐹) | 
| 106 | 2, 3, 21, 22, 8, 10, 6, 4, 105 | hlln 28616 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ (𝐹𝐿𝐷)) | 
| 107 | 2, 3, 4, 5, 7, 9, 75 | tglinerflx1 28642 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐹𝐿𝐷)) | 
| 108 | 107 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ (𝐹𝐿𝐷)) | 
| 109 | 2, 3, 21, 5, 14, 15, 16, 9, 11, 7, 17 | cgrane4 28824 | . . . . . . 7
⊢ (𝜑 → 𝐸 ≠ 𝐹) | 
| 110 | 109 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐸 ≠ 𝐹) | 
| 111 | 2, 3, 21, 22, 8, 12, 6, 4, 44 | hlln 28616 | . . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ (𝐹𝐿𝐸)) | 
| 112 | 2, 3, 4, 6, 12, 8,
22, 110, 111 | lncom 28631 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 ∈ (𝐸𝐿𝐹)) | 
| 113 | 2, 3, 4, 6, 12, 8,
110 | tglinerflx2 28643 | . . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝐹 ∈ (𝐸𝐿𝐹)) | 
| 114 | 2, 3, 4, 6, 8, 10,
12, 8, 20, 106, 108, 112, 113 | tglineinteq 28654 | . . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → 𝑓 = 𝐹) | 
| 115 | 114 | oveq2d 7448 | . . 3
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐸 − 𝑓) = (𝐸 − 𝐹)) | 
| 116 | 1, 115 | eqtr3d 2778 | . 2
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑃) ∧ (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) → (𝐵 − 𝐶) = (𝐸 − 𝐹)) | 
| 117 | 109 | necomd 2995 | . . 3
⊢ (𝜑 → 𝐹 ≠ 𝐸) | 
| 118 | 2, 3, 21, 11, 15, 16, 5, 7, 13, 117, 49 | hlcgrex 28625 | . 2
⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (𝑓((hlG‘𝐺)‘𝐸)𝐹 ∧ (𝐸 − 𝑓) = (𝐵 − 𝐶))) | 
| 119 | 116, 118 | r19.29a 3161 | 1
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐸 − 𝐹)) |