| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | trgcopy.p | . . . . . . 7
⊢ 𝑃 = (Base‘𝐺) | 
| 2 |  | trgcopy.m | . . . . . . 7
⊢  − =
(dist‘𝐺) | 
| 3 |  | eqid 2736 | . . . . . . 7
⊢
(cgrG‘𝐺) =
(cgrG‘𝐺) | 
| 4 |  | trgcopy.g | . . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ TarskiG) | 
| 5 | 4 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG) | 
| 6 | 5 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐺 ∈ TarskiG) | 
| 7 | 6 | ad2antrr 726 | . . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐺 ∈ TarskiG) | 
| 8 | 7 | adantr 480 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺 ∈ TarskiG) | 
| 9 |  | trgcopy.a | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑃) | 
| 10 | 9 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃) | 
| 11 | 10 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐴 ∈ 𝑃) | 
| 12 | 11 | ad3antrrr 730 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ∈ 𝑃) | 
| 13 |  | trgcopy.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑃) | 
| 14 | 13 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃) | 
| 15 | 14 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐵 ∈ 𝑃) | 
| 16 | 15 | ad3antrrr 730 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐵 ∈ 𝑃) | 
| 17 |  | trgcopy.c | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ 𝑃) | 
| 18 | 17 | ad6antr 736 | . . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐶 ∈ 𝑃) | 
| 19 | 18 | adantr 480 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ∈ 𝑃) | 
| 20 |  | trgcopy.d | . . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ 𝑃) | 
| 21 | 20 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐷 ∈ 𝑃) | 
| 22 | 21 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐷 ∈ 𝑃) | 
| 23 | 22 | ad3antrrr 730 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐷 ∈ 𝑃) | 
| 24 |  | trgcopy.e | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ 𝑃) | 
| 25 | 24 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐸 ∈ 𝑃) | 
| 26 | 25 | ad2antrr 726 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐸 ∈ 𝑃) | 
| 27 | 26 | ad3antrrr 730 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ∈ 𝑃) | 
| 28 |  | simprl 770 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ 𝑃) | 
| 29 |  | trgcopy.3 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 30 | 29 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 31 | 30 | ad5antr 734 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴 − 𝐵) = (𝐷 − 𝐸)) | 
| 32 |  | trgcopy.i | . . . . . . . 8
⊢ 𝐼 = (Itv‘𝐺) | 
| 33 |  | trgcopy.l | . . . . . . . . . . 11
⊢ 𝐿 = (LineG‘𝐺) | 
| 34 |  | trgcopy.1 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 35 | 1, 33, 32, 4, 13, 17, 9, 34 | ncoltgdim2 28574 | . . . . . . . . . 10
⊢ (𝜑 → 𝐺DimTarskiG≥2) | 
| 36 | 35 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐺DimTarskiG≥2) | 
| 37 | 36 | ad3antrrr 730 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺DimTarskiG≥2) | 
| 38 | 1, 32, 33, 4, 9, 13, 17, 34 | ncolne1 28634 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ≠ 𝐵) | 
| 39 | 1, 32, 33, 4, 9, 13, 38 | tgelrnln 28639 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿) | 
| 40 | 39 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴𝐿𝐵) ∈ ran 𝐿) | 
| 41 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ (𝐴𝐿𝐵)) | 
| 42 | 1, 33, 32, 5, 40, 41 | tglnpt 28558 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ 𝑃) | 
| 43 | 42 | ad2antrr 726 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝑥 ∈ 𝑃) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ∈ 𝑃) | 
| 45 | 44 | adantr 480 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ 𝑃) | 
| 46 |  | simplr 768 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝑦 ∈ 𝑃) | 
| 47 | 46 | ad2antrr 726 | . . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑦 ∈ 𝑃) | 
| 48 | 47 | adantr 480 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ 𝑃) | 
| 49 | 41 | ad5antr 734 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐴𝐿𝐵)) | 
| 50 | 38 | ad7antr 738 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ≠ 𝐵) | 
| 51 | 1, 32, 33, 8, 12, 16, 50 | tglinecom 28644 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴)) | 
| 52 | 49, 51 | eleqtrd 2842 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐵𝐿𝐴)) | 
| 53 |  | simp-6r 787 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 54 | 33, 8, 53 | perpln1 28719 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) ∈ ran 𝐿) | 
| 55 | 40 | ad5antr 734 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) ∈ ran 𝐿) | 
| 56 | 1, 2, 32, 33, 8, 54, 55, 53 | perpcom 28722 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝑥)) | 
| 57 | 1, 33, 32, 4, 13, 17, 9, 34 | ncolrot2 28572 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 58 |  | ioran 985 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
(𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ↔ (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵)) | 
| 59 | 57, 58 | sylib 218 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵)) | 
| 60 | 59 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵)) | 
| 61 | 60 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ¬ 𝐶 ∈ (𝐴𝐿𝐵)) | 
| 62 |  | nelne2 3039 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐶 ∈ (𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶) | 
| 63 | 41, 61, 62 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶) | 
| 64 | 63 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ≠ 𝐶) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ≠ 𝐶) | 
| 66 | 65 | necomd 2995 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ≠ 𝑥) | 
| 67 | 1, 32, 33, 8, 19, 45, 66 | tglinecom 28644 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) = (𝑥𝐿𝐶)) | 
| 68 | 56, 51, 67 | 3brtr3d 5173 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑥𝐿𝐶)) | 
| 69 | 1, 2, 32, 33, 8, 16, 12, 52, 19, 68 | perprag 28735 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐵𝑥𝐶”〉 ∈ (∟G‘𝐺)) | 
| 70 |  | trgcopy.f | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ 𝑃) | 
| 71 |  | trgcopy.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹)) | 
| 72 | 1, 32, 33, 4, 20, 24, 70, 71 | ncolne1 28634 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ≠ 𝐸) | 
| 73 | 72 | necomd 2995 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ≠ 𝐷) | 
| 74 | 73 | ad7antr 738 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ≠ 𝐷) | 
| 75 | 72 | ad4antr 732 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐷 ≠ 𝐸) | 
| 76 | 75 | neneqd 2944 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → ¬ 𝐷 = 𝐸) | 
| 77 | 41 | orcd 873 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) | 
| 78 | 1, 33, 32, 5, 10, 14, 42, 77 | colrot2 28569 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝑥𝐿𝐴) ∨ 𝑥 = 𝐴)) | 
| 79 | 1, 33, 32, 5, 42, 10, 14, 78 | colcom 28567 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥)) | 
| 80 | 79 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥)) | 
| 81 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) | 
| 82 | 1, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 80, 81 | lnxfr 28575 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (𝐸 ∈ (𝐷𝐿𝑦) ∨ 𝐷 = 𝑦)) | 
| 83 | 1, 33, 32, 6, 22, 46, 26, 82 | colrot2 28569 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 84 | 1, 33, 32, 6, 26, 22, 46, 83 | colcom 28567 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 85 | 84 | orcomd 871 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (𝐷 = 𝐸 ∨ 𝑦 ∈ (𝐷𝐿𝐸))) | 
| 86 | 85 | ord 864 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (¬ 𝐷 = 𝐸 → 𝑦 ∈ (𝐷𝐿𝐸))) | 
| 87 | 76, 86 | mpd 15 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝑦 ∈ (𝐷𝐿𝐸)) | 
| 88 | 87 | ad3antrrr 730 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐷𝐿𝐸)) | 
| 89 | 1, 32, 33, 8, 27, 23, 48, 74, 88 | lncom 28631 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐸𝐿𝐷)) | 
| 90 |  | simprrr 781 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦 − 𝑓) = (𝑥 − 𝐶)) | 
| 91 | 90 | eqcomd 2742 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐶) = (𝑦 − 𝑓)) | 
| 92 | 1, 2, 32, 8, 45, 19, 48, 28, 91, 65 | tgcgrneq 28492 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑓) | 
| 93 | 1, 32, 33, 8, 48, 28, 92 | tgelrnln 28639 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓) ∈ ran 𝐿) | 
| 94 | 1, 32, 33, 8, 27, 23, 74 | tgelrnln 28639 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) ∈ ran 𝐿) | 
| 95 |  | simpllr 775 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ∈ 𝑃) | 
| 96 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ∈ 𝑃) | 
| 97 |  | simprl 770 | . . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦)) | 
| 98 | 33, 7, 97 | perpln2 28720 | . . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝑞𝐿𝑦) ∈ ran 𝐿) | 
| 99 | 1, 32, 33, 7, 96, 47, 98 | tglnne 28637 | . . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ≠ 𝑦) | 
| 100 | 99 | adantr 480 | . . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ≠ 𝑦) | 
| 101 | 100 | necomd 2995 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑞) | 
| 102 | 1, 32, 33, 8, 48, 95, 101 | tgelrnln 28639 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) ∈ ran 𝐿) | 
| 103 | 97 | adantr 480 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦)) | 
| 104 | 1, 32, 33, 8, 27, 23, 74 | tglinecom 28644 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) = (𝐷𝐿𝐸)) | 
| 105 | 1, 32, 33, 8, 48, 95, 101 | tglinecom 28644 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) = (𝑞𝐿𝑦)) | 
| 106 | 103, 104,
105 | 3brtr4d 5174 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑞)) | 
| 107 | 1, 2, 32, 33, 8, 94, 102, 106 | perpcom 28722 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞)(⟂G‘𝐺)(𝐸𝐿𝐷)) | 
| 108 |  | trgcopy.k | . . . . . . . . . . . . . 14
⊢ 𝐾 = (hlG‘𝐺) | 
| 109 |  | simprrl 780 | . . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓(𝐾‘𝑦)𝑞) | 
| 110 | 1, 32, 108, 28, 95, 48, 8, 33, 109 | hlln 28616 | . . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑞𝐿𝑦)) | 
| 111 | 1, 32, 33, 8, 48, 95, 28, 101, 110 | lncom 28631 | . . . . . . . . . . . 12
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑦𝐿𝑞)) | 
| 112 | 111 | orcd 873 | . . . . . . . . . . 11
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑓 ∈ (𝑦𝐿𝑞) ∨ 𝑦 = 𝑞)) | 
| 113 | 1, 2, 32, 33, 8, 48, 95, 28, 107, 112, 92 | colperp 28738 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓)(⟂G‘𝐺)(𝐸𝐿𝐷)) | 
| 114 | 1, 2, 32, 33, 8, 93, 94, 113 | perpcom 28722 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑓)) | 
| 115 | 1, 2, 32, 33, 8, 27, 23, 89, 28, 114 | perprag 28735 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐸𝑦𝑓”〉 ∈ (∟G‘𝐺)) | 
| 116 | 81 | ad3antrrr 730 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) | 
| 117 | 1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116 | cgr3simp2 28530 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝑥) = (𝐸 − 𝑦)) | 
| 118 | 1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 115, 117, 91 | hypcgr 28810 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝐶) = (𝐸 − 𝑓)) | 
| 119 |  | eqid 2736 | . . . . . . . . 9
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) | 
| 120 | 51, 68 | eqbrtrd 5164 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑥𝐿𝐶)) | 
| 121 | 1, 2, 32, 33, 8, 12, 16, 49, 19, 120 | perprag 28735 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐴𝑥𝐶”〉 ∈ (∟G‘𝐺)) | 
| 122 | 1, 2, 32, 33, 119, 8, 12, 45, 19, 121 | ragcom 28707 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐶𝑥𝐴”〉 ∈ (∟G‘𝐺)) | 
| 123 | 104, 114 | eqbrtrrd 5166 | . . . . . . . . . 10
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑦𝐿𝑓)) | 
| 124 | 1, 2, 32, 33, 8, 23, 27, 88, 28, 123 | perprag 28735 | . . . . . . . . 9
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐷𝑦𝑓”〉 ∈ (∟G‘𝐺)) | 
| 125 | 1, 2, 32, 33, 119, 8, 23, 48, 28, 124 | ragcom 28707 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝑓𝑦𝐷”〉 ∈ (∟G‘𝐺)) | 
| 126 | 1, 2, 32, 8, 45, 19, 48, 28, 91 | tgcgrcomlr 28489 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝑥) = (𝑓 − 𝑦)) | 
| 127 | 1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116 | cgr3simp3 28531 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐴) = (𝑦 − 𝐷)) | 
| 128 | 1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 122, 125, 126, 127 | hypcgr 28810 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝐴) = (𝑓 − 𝐷)) | 
| 129 | 1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 118, 128 | trgcgr 28525 | . . . . . 6
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉) | 
| 130 | 1, 32, 33, 4, 20, 24, 72 | tgelrnln 28639 | . . . . . . . . 9
⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿) | 
| 131 | 130 | ad4antr 732 | . . . . . . . 8
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → (𝐷𝐿𝐸) ∈ ran 𝐿) | 
| 132 | 131 | ad3antrrr 730 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸) ∈ ran 𝐿) | 
| 133 |  | simpl 482 | . . . . . . . . . . 11
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑤 = 𝑘) | 
| 134 | 133 | eleq1d 2825 | . . . . . . . . . 10
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))) | 
| 135 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑣 = 𝑙) | 
| 136 | 135 | eleq1d 2825 | . . . . . . . . . 10
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))) | 
| 137 | 134, 136 | anbi12d 632 | . . . . . . . . 9
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ↔ (𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))) | 
| 138 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗) | 
| 139 |  | simpll 766 | . . . . . . . . . . . 12
⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑤 = 𝑘) | 
| 140 |  | simplr 768 | . . . . . . . . . . . 12
⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑣 = 𝑙) | 
| 141 | 139, 140 | oveq12d 7450 | . . . . . . . . . . 11
⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑤𝐼𝑣) = (𝑘𝐼𝑙)) | 
| 142 | 138, 141 | eleq12d 2834 | . . . . . . . . . 10
⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑧 ∈ (𝑤𝐼𝑣) ↔ 𝑗 ∈ (𝑘𝐼𝑙))) | 
| 143 | 142 | cbvrexdva 3239 | . . . . . . . . 9
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣) ↔ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))) | 
| 144 | 137, 143 | anbi12d 632 | . . . . . . . 8
⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣)) ↔ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙)))) | 
| 145 | 144 | cbvopabv 5215 | . . . . . . 7
⊢
{〈𝑤, 𝑣〉 ∣ ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣))} = {〈𝑘, 𝑙〉 ∣ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))} | 
| 146 | 8 | adantr 480 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐺 ∈ TarskiG) | 
| 147 | 19 | adantr 480 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐶 ∈ 𝑃) | 
| 148 | 16 | adantr 480 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐵 ∈ 𝑃) | 
| 149 | 12 | adantr 480 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐴 ∈ 𝑃) | 
| 150 | 23 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐷 ∈ 𝑃) | 
| 151 | 27 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ∈ 𝑃) | 
| 152 | 28 | adantr 480 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ 𝑃) | 
| 153 | 73 | ad8antr 740 | . . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ≠ 𝐷) | 
| 154 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐷𝐿𝐸)) | 
| 155 | 1, 32, 33, 146, 151, 150, 152, 153, 154 | lncom 28631 | . . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐸𝐿𝐷)) | 
| 156 | 155 | orcd 873 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝑓 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷)) | 
| 157 | 1, 33, 32, 146, 151, 150, 152, 156 | colrot1 28568 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐸 ∈ (𝐷𝐿𝑓) ∨ 𝐷 = 𝑓)) | 
| 158 | 129 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉) | 
| 159 | 1, 2, 32, 3, 146, 149, 148, 147, 150, 151, 152, 158 | trgcgrcom 28537 | . . . . . . . . . . . 12
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 〈“𝐷𝐸𝑓”〉(cgrG‘𝐺)〈“𝐴𝐵𝐶”〉) | 
| 160 | 1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159 | lnxfr 28575 | . . . . . . . . . . 11
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) | 
| 161 | 1, 33, 32, 146, 149, 147, 148, 160 | colrot1 28568 | . . . . . . . . . 10
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵)) | 
| 162 | 1, 33, 32, 146, 147, 148, 149, 161 | colcom 28567 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 163 | 34 | ad8antr 740 | . . . . . . . . 9
⊢
(((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) | 
| 164 | 162, 163 | pm2.65da 816 | . . . . . . . 8
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ¬ 𝑓 ∈ (𝐷𝐿𝐸)) | 
| 165 | 1, 32, 33, 8, 132, 48, 145, 108, 88, 28, 95, 164, 109 | hphl 28780 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞) | 
| 166 | 70 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → 𝐹 ∈ 𝑃) | 
| 167 | 166 | ad2antrr 726 | . . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐹 ∈ 𝑃) | 
| 168 | 167 | adantr 480 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐹 ∈ 𝑃) | 
| 169 |  | simplrr 777 | . . . . . . 7
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) | 
| 170 | 1, 32, 33, 8, 132, 28, 145, 95, 165, 168, 169 | hpgtr 28777 | . . . . . 6
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹) | 
| 171 | 129, 170 | jca 511 | . . . . 5
⊢
((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | 
| 172 | 1, 32, 108, 47, 44, 18, 7, 96, 2, 99, 64 | hlcgrex 28625 | . . . . 5
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶))) | 
| 173 | 171, 172 | reximddv 3170 | . . . 4
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | 
| 174 | 1, 33, 32, 4, 24, 70, 20, 71 | ncolrot2 28572 | . . . . . . . 8
⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) | 
| 175 |  | ioran 985 | . . . . . . . 8
⊢ (¬
(𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸)) | 
| 176 | 174, 175 | sylib 218 | . . . . . . 7
⊢ (𝜑 → (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸)) | 
| 177 | 176 | simpld 494 | . . . . . 6
⊢ (𝜑 → ¬ 𝐹 ∈ (𝐷𝐿𝐸)) | 
| 178 | 177 | ad4antr 732 | . . . . 5
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → ¬ 𝐹 ∈ (𝐷𝐿𝐸)) | 
| 179 | 1, 2, 32, 33, 6, 36, 131, 145, 87, 166, 178 | lnperpex 28812 | . . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → ∃𝑞 ∈ 𝑃 ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | 
| 180 | 173, 179 | r19.29a 3161 | . . 3
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | 
| 181 | 1, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 79, 30 | lnext 28576 | . . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑦 ∈ 𝑃 〈“𝐴𝐵𝑥”〉(cgrG‘𝐺)〈“𝐷𝐸𝑦”〉) | 
| 182 | 180, 181 | r19.29a 3161 | . 2
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) | 
| 183 | 1, 2, 32, 33, 4, 39, 17, 60 | footex 28730 | . 2
⊢ (𝜑 → ∃𝑥 ∈ (𝐴𝐿𝐵)(𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) | 
| 184 | 182, 183 | r19.29a 3161 | 1
⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (〈“𝐴𝐵𝐶”〉(cgrG‘𝐺)〈“𝐷𝐸𝑓”〉 ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) |