| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dfcgra2.p | . . . 4
⊢ 𝑃 = (Base‘𝐺) | 
| 2 |  | dfcgra2.i | . . . 4
⊢ 𝐼 = (Itv‘𝐺) | 
| 3 |  | acopyeu.k | . . . 4
⊢ 𝐾 = (hlG‘𝐺) | 
| 4 |  | acopyeu.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝑃) | 
| 5 | 4 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑋 ∈ 𝑃) | 
| 6 | 5 | ad3antrrr 730 | . . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋 ∈ 𝑃) | 
| 7 |  | simplr 768 | . . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦 ∈ 𝑃) | 
| 8 |  | acopyeu.y | . . . . . 6
⊢ (𝜑 → 𝑌 ∈ 𝑃) | 
| 9 | 8 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑌 ∈ 𝑃) | 
| 10 | 9 | ad3antrrr 730 | . . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑌 ∈ 𝑃) | 
| 11 |  | dfcgra2.g | . . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 12 | 11 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐺 ∈ TarskiG) | 
| 13 | 12 | ad3antrrr 730 | . . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐺 ∈ TarskiG) | 
| 14 |  | dfcgra2.e | . . . . . 6
⊢ (𝜑 → 𝐸 ∈ 𝑃) | 
| 15 | 14 | ad2antrr 726 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐸 ∈ 𝑃) | 
| 16 | 15 | ad3antrrr 730 | . . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐸 ∈ 𝑃) | 
| 17 |  | dfcgra2.m | . . . . . . 7
⊢  − =
(dist‘𝐺) | 
| 18 |  | acopy.l | . . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) | 
| 19 |  | dfcgra2.a | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 20 | 19 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐴 ∈ 𝑃) | 
| 21 | 20 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐴 ∈ 𝑃) | 
| 22 |  | dfcgra2.b | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 23 | 22 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐵 ∈ 𝑃) | 
| 24 | 23 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐵 ∈ 𝑃) | 
| 25 |  | dfcgra2.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 26 | 25 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐶 ∈ 𝑃) | 
| 27 | 26 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐶 ∈ 𝑃) | 
| 28 |  | simplr 768 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑 ∈ 𝑃) | 
| 29 | 28 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑑 ∈ 𝑃) | 
| 30 |  | dfcgra2.f | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝑃) | 
| 31 | 30 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐹 ∈ 𝑃) | 
| 32 | 31 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐹 ∈ 𝑃) | 
| 33 |  | acopy.1 | . . . . . . . . 9
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 34 | 33 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 35 | 34 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 36 |  | dfcgra2.d | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 37 | 36 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐷 ∈ 𝑃) | 
| 38 |  | acopy.2 | . . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) | 
| 39 | 38 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) | 
| 40 |  | simprl 770 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑(𝐾‘𝐸)𝐷) | 
| 41 | 1, 2, 3, 28, 37, 15, 12, 18, 40 | hlln 28616 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑 ∈ (𝐷𝐿𝐸)) | 
| 42 | 1, 2, 3, 28, 37, 15, 12, 40 | hlne1 28614 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑑 ≠ 𝐸) | 
| 43 | 1, 2, 18, 12, 37, 15, 31, 28, 39, 41, 42 | ncolncol 28655 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) | 
| 44 | 43 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑑 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) | 
| 45 |  | simprr 772 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐸 − 𝑑) = (𝐵 − 𝐴)) | 
| 46 | 1, 17, 2, 12, 15, 28, 23, 20, 45 | tgcgrcomlr 28489 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝑑 − 𝐸) = (𝐴 − 𝐵)) | 
| 47 | 46 | eqcomd 2742 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐴 − 𝐵) = (𝑑 − 𝐸)) | 
| 48 | 47 | ad3antrrr 730 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝐴 − 𝐵) = (𝑑 − 𝐸)) | 
| 49 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑢 = 𝑎) | 
| 50 | 49 | eleq1d 2825 | . . . . . . . . . 10
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ↔ 𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)))) | 
| 51 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → 𝑣 = 𝑏) | 
| 52 | 51 | eleq1d 2825 | . . . . . . . . . 10
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ↔ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸)))) | 
| 53 | 50, 52 | anbi12d 632 | . . . . . . . . 9
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ↔ (𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))))) | 
| 54 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑤 = 𝑡) | 
| 55 |  | simpll 766 | . . . . . . . . . . . 12
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑢 = 𝑎) | 
| 56 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → 𝑣 = 𝑏) | 
| 57 | 55, 56 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → (𝑢𝐼𝑣) = (𝑎𝐼𝑏)) | 
| 58 | 54, 57 | eleq12d 2834 | . . . . . . . . . 10
⊢ (((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) ∧ 𝑤 = 𝑡) → (𝑤 ∈ (𝑢𝐼𝑣) ↔ 𝑡 ∈ (𝑎𝐼𝑏))) | 
| 59 | 58 | cbvrexdva 3239 | . . . . . . . . 9
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣) ↔ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))) | 
| 60 | 53, 59 | anbi12d 632 | . . . . . . . 8
⊢ ((𝑢 = 𝑎 ∧ 𝑣 = 𝑏) → (((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣)) ↔ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏)))) | 
| 61 | 60 | cbvopabv 5215 | . . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑤 ∈ (𝑑𝐿𝐸)𝑤 ∈ (𝑢𝐼𝑣))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ (𝑑𝐿𝐸)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑑𝐿𝐸))) ∧ ∃𝑡 ∈ (𝑑𝐿𝐸)𝑡 ∈ (𝑎𝐼𝑏))} | 
| 62 |  | simpllr 775 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 ∈ 𝑃) | 
| 63 |  | simprll 778 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉) | 
| 64 |  | simprrl 780 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉) | 
| 65 | 1, 2, 18, 12, 28, 15, 42 | tgelrnln 28639 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝑑𝐿𝐸) ∈ ran 𝐿) | 
| 66 | 65 | ad3antrrr 730 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝑑𝐿𝐸) ∈ ran 𝐿) | 
| 67 | 1, 2, 18, 12, 28, 15, 42 | tglinerflx2 28643 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐸 ∈ (𝑑𝐿𝐸)) | 
| 68 | 67 | ad3antrrr 730 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐸 ∈ (𝑑𝐿𝐸)) | 
| 69 | 37 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝐷 ∈ 𝑃) | 
| 70 |  | acopyeu.1 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) | 
| 71 | 1, 18, 2, 11, 22, 25, 19, 33 | ncolrot2 28572 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 72 | 1, 2, 17, 11, 19, 22, 25, 36, 14, 4, 70, 18, 71 | cgrancol 28838 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝑋 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 73 | 1, 18, 2, 11, 36, 14, 4, 72 | ncolcom 28570 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 74 | 73 | ad5antr 734 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑋 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 75 |  | simprlr 779 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥(𝐾‘𝐸)𝑋) | 
| 76 | 1, 2, 3, 62, 6, 16, 13, 18, 75 | hlln 28616 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 ∈ (𝑋𝐿𝐸)) | 
| 77 | 1, 2, 3, 62, 6, 16, 13, 75 | hlne1 28614 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 ≠ 𝐸) | 
| 78 | 1, 2, 18, 13, 6, 16, 69, 62, 74, 76, 77 | ncolncol 28655 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑥 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 79 | 1, 18, 2, 13, 16, 69, 62, 78 | ncolcom 28570 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 80 |  | pm2.45 881 | . . . . . . . . . . 11
⊢ (¬
(𝑥 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) → ¬ 𝑥 ∈ (𝐷𝐿𝐸)) | 
| 81 | 79, 80 | syl 17 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑥 ∈ (𝐷𝐿𝐸)) | 
| 82 | 1, 2, 18, 11, 36, 14, 30, 38 | ncolne1 28634 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ≠ 𝐸) | 
| 83 | 1, 2, 18, 11, 36, 14, 82 | tgelrnln 28639 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿) | 
| 84 | 83 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐷𝐿𝐸) ∈ ran 𝐿) | 
| 85 | 1, 2, 18, 11, 36, 14, 82 | tglinerflx2 28643 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ (𝐷𝐿𝐸)) | 
| 86 | 85 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐸 ∈ (𝐷𝐿𝐸)) | 
| 87 | 1, 2, 18, 12, 28, 15, 42, 42, 84, 41, 86 | tglinethru 28645 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (𝐷𝐿𝐸) = (𝑑𝐿𝐸)) | 
| 88 | 87 | ad3antrrr 730 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → (𝐷𝐿𝐸) = (𝑑𝐿𝐸)) | 
| 89 | 81, 88 | neleqtrd 2862 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑥 ∈ (𝑑𝐿𝐸)) | 
| 90 | 1, 2, 18, 13, 66, 16, 61, 3, 68, 62, 6, 89, 75 | hphl 28780 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥((hpG‘𝐺)‘(𝑑𝐿𝐸))𝑋) | 
| 91 | 87 | fveq2d 6909 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ((hpG‘𝐺)‘(𝐷𝐿𝐸)) = ((hpG‘𝐺)‘(𝑑𝐿𝐸))) | 
| 92 | 91 | ad3antrrr 730 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ((hpG‘𝐺)‘(𝐷𝐿𝐸)) = ((hpG‘𝐺)‘(𝑑𝐿𝐸))) | 
| 93 |  | acopyeu.3 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) | 
| 94 | 93 | ad5antr 734 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) | 
| 95 | 92, 94 | breqdi 5157 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) | 
| 96 | 1, 2, 18, 13, 66, 62, 61, 6, 90, 32, 95 | hpgtr 28777 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) | 
| 97 |  | acopyeu.2 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑌”〉) | 
| 98 | 1, 2, 17, 11, 19, 22, 25, 36, 14, 8, 97, 18, 71 | cgrancol 28838 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝑌 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 99 | 1, 18, 2, 11, 36, 14, 8, 98 | ncolcom 28570 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ (𝑌 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 100 | 99 | ad5antr 734 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑌 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 101 |  | simprrr 781 | . . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦(𝐾‘𝐸)𝑌) | 
| 102 | 1, 2, 3, 7, 10, 16, 13, 18, 101 | hlln 28616 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦 ∈ (𝑌𝐿𝐸)) | 
| 103 | 1, 2, 3, 7, 10, 16, 13, 101 | hlne1 28614 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦 ≠ 𝐸) | 
| 104 | 1, 2, 18, 13, 10, 16, 69, 7, 100, 102, 103 | ncolncol 28655 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 105 | 1, 18, 2, 13, 16, 69, 7, 104 | ncolcom 28570 | . . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 106 |  | pm2.45 881 | . . . . . . . . . . 11
⊢ (¬
(𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) → ¬ 𝑦 ∈ (𝐷𝐿𝐸)) | 
| 107 | 105, 106 | syl 17 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑦 ∈ (𝐷𝐿𝐸)) | 
| 108 | 107, 88 | neleqtrd 2862 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → ¬ 𝑦 ∈ (𝑑𝐿𝐸)) | 
| 109 | 1, 2, 18, 13, 66, 16, 61, 3, 68, 7, 10, 108, 101 | hphl 28780 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦((hpG‘𝐺)‘(𝑑𝐿𝐸))𝑌) | 
| 110 |  | acopyeu.4 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) | 
| 111 | 110 | ad5antr 734 | . . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑌((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) | 
| 112 | 92, 111 | breqdi 5157 | . . . . . . . 8
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑌((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) | 
| 113 | 1, 2, 18, 13, 66, 7, 61, 10, 109, 32, 112 | hpgtr 28777 | . . . . . . 7
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦((hpG‘𝐺)‘(𝑑𝐿𝐸))𝐹) | 
| 114 | 1, 17, 2, 18, 3, 13, 21, 24, 27, 29, 16, 32, 35, 44, 48, 61, 62, 7, 63, 64, 96, 113 | trgcopyeulem 28814 | . . . . . 6
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑥 = 𝑦) | 
| 115 | 114, 75 | eqbrtrrd 5166 | . . . . 5
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑦(𝐾‘𝐸)𝑋) | 
| 116 | 1, 2, 3, 7, 6, 16,
13, 115 | hlcomd 28613 | . . . 4
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋(𝐾‘𝐸)𝑦) | 
| 117 | 1, 2, 3, 6, 7, 10,
13, 16, 116, 101 | hltr 28619 | . . 3
⊢
((((((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) ∧ 𝑥 ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) → 𝑋(𝐾‘𝐸)𝑌) | 
| 118 | 70 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑋”〉) | 
| 119 | 1, 2, 3, 12, 20, 23, 26, 37, 15, 5, 118, 28, 40 | cgrahl1 28825 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑋”〉) | 
| 120 | 1, 2, 18, 11, 19, 22, 25, 33 | ncolne1 28634 | . . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| 121 | 120 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝐴 ≠ 𝐵) | 
| 122 | 1, 2, 3, 12, 20, 23, 26, 28, 15, 5, 17, 121, 47 | iscgra1 28819 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑋”〉 ↔ ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋))) | 
| 123 | 119, 122 | mpbid 232 | . . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋)) | 
| 124 | 97 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝑌”〉) | 
| 125 | 1, 2, 3, 12, 20, 23, 26, 37, 15, 9, 124, 28, 40 | cgrahl1 28825 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑌”〉) | 
| 126 | 1, 2, 3, 12, 20, 23, 26, 28, 15, 9, 17, 121, 47 | iscgra1 28819 | . . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → (〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝑑𝐸𝑌”〉 ↔ ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) | 
| 127 | 125, 126 | mpbid 232 | . . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌)) | 
| 128 |  | reeanv 3228 | . . . 4
⊢
(∃𝑥 ∈
𝑃 ∃𝑦 ∈ 𝑃 ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌)) ↔ (∃𝑥 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ ∃𝑦 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) | 
| 129 | 123, 127,
128 | sylanbrc 583 | . . 3
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → ∃𝑥 ∈ 𝑃 ∃𝑦 ∈ 𝑃 ((〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑥”〉 ∧ 𝑥(𝐾‘𝐸)𝑋) ∧ (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝑑𝐸𝑦”〉 ∧ 𝑦(𝐾‘𝐸)𝑌))) | 
| 130 | 117, 129 | r19.29vva 3215 | . 2
⊢ (((𝜑 ∧ 𝑑 ∈ 𝑃) ∧ (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) → 𝑋(𝐾‘𝐸)𝑌) | 
| 131 | 120 | necomd 2995 | . . 3
⊢ (𝜑 → 𝐵 ≠ 𝐴) | 
| 132 | 1, 2, 3, 14, 22, 19, 11, 36, 17, 82, 131 | hlcgrex 28625 | . 2
⊢ (𝜑 → ∃𝑑 ∈ 𝑃 (𝑑(𝐾‘𝐸)𝐷 ∧ (𝐸 − 𝑑) = (𝐵 − 𝐴))) | 
| 133 | 130, 132 | r19.29a 3161 | 1
⊢ (𝜑 → 𝑋(𝐾‘𝐸)𝑌) |