trgcopy - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > trgcopy		Structured version Visualization version GIF version

Theorem trgcopy 27165

Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: existence part. First part of Theorem 10.16 of [Schwabhauser] p. 92. (Contributed by Thierry Arnoux, 4-Aug-2020.)

**Hypotheses**
Ref	Expression
trgcopy.p	⊢ 𝑃 = (Base‘𝐺)
trgcopy.m	⊢ − = (dist‘𝐺)
trgcopy.i	⊢ 𝐼 = (Itv‘𝐺)
trgcopy.l	⊢ 𝐿 = (LineG‘𝐺)
trgcopy.k	⊢ 𝐾 = (hlG‘𝐺)
trgcopy.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
trgcopy.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
trgcopy.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
trgcopy.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
trgcopy.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
trgcopy.e	⊢ (𝜑 → 𝐸 ∈ 𝑃)
trgcopy.f	⊢ (𝜑 → 𝐹 ∈ 𝑃)
trgcopy.1	⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
trgcopy.2	⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
trgcopy.3	⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))

**Assertion**
Ref	Expression
trgcopy	⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))

Distinct variable groups: − ,𝑓 𝐴,𝑓 𝐵,𝑓 𝐶,𝑓 𝐷,𝑓 𝑓,𝐸 𝑓,𝐹 𝑓,𝐺 𝑓,𝐼 𝑓,𝐿 𝑃,𝑓 𝜑,𝑓 𝑓,𝐾

Proof of Theorem trgcopy Dummy variables 𝑗 𝑘 𝑙 𝑞 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		trgcopy.p	. . . . . . 7 ⊢ 𝑃 = (Base‘𝐺)
2		trgcopy.m	. . . . . . 7 ⊢ − = (dist‘𝐺)
3		eqid 2738	. . . . . . 7 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
4		trgcopy.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
6	5	ad2antrr 723	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
7	6	ad2antrr 723	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐺 ∈ TarskiG)
8	7	adantr 481	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺 ∈ TarskiG)
9		trgcopy.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10	9	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
11	10	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴 ∈ 𝑃)
12	11	ad3antrrr 727	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ∈ 𝑃)
13		trgcopy.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
14	13	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
15	14	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵 ∈ 𝑃)
16	15	ad3antrrr 727	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐵 ∈ 𝑃)
17		trgcopy.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
18	17	ad6antr 733	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐶 ∈ 𝑃)
19	18	adantr 481	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ∈ 𝑃)
20		trgcopy.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
21	20	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐷 ∈ 𝑃)
22	21	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ∈ 𝑃)
23	22	ad3antrrr 727	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐷 ∈ 𝑃)
24		trgcopy.e	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
25	24	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐸 ∈ 𝑃)
26	25	ad2antrr 723	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸 ∈ 𝑃)
27	26	ad3antrrr 727	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ∈ 𝑃)
28		simprl 768	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ 𝑃)
29		trgcopy.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))
30	29	ad2antrr 723	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
31	30	ad5antr 731	. . . . . . 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 26926	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
36	35	ad4antr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺Dim_TarskiG≥2)
37	36	ad3antrrr 727	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺Dim_TarskiG≥2)
38	1, 32, 33, 4, 9, 13, 17, 34	ncolne1 26986	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	1, 32, 33, 4, 9, 13, 38	tgelrnln 26991	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
40	39	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴𝐿𝐵) ∈ ran 𝐿)
41		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ (𝐴𝐿𝐵))
42	1, 33, 32, 5, 40, 41	tglnpt 26910	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ 𝑃)
43	42	ad2antrr 723	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑥 ∈ 𝑃)
44	43	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ∈ 𝑃)
45	44	adantr 481	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ 𝑃)
46		simplr 766	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ 𝑃)
47	46	ad2antrr 723	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑦 ∈ 𝑃)
48	47	adantr 481	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ 𝑃)
49	41	ad5antr 731	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐴𝐿𝐵))
50	38	ad7antr 735	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ≠ 𝐵)
51	1, 32, 33, 8, 12, 16, 50	tglinecom 26996	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
52	49, 51	eleqtrd 2841	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐵𝐿𝐴))
53		simp-6r 785	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
54	33, 8, 53	perpln1 27071	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
55	40	ad5antr 731	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) ∈ ran 𝐿)
56	1, 2, 32, 33, 8, 54, 55, 53	perpcom 27074	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝑥))
57	1, 33, 32, 4, 13, 17, 9, 34	ncolrot2 26924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
58		ioran 981	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ↔ (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
59	57, 58	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
60	59	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
61	60	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
62		nelne2 3042	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐶 ∈ (𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
63	41, 61, 62	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
64	63	ad4antr 729	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ≠ 𝐶)
65	64	adantr 481	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ≠ 𝐶)
66	65	necomd 2999	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ≠ 𝑥)
67	1, 32, 33, 8, 19, 45, 66	tglinecom 26996	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) = (𝑥𝐿𝐶))
68	56, 51, 67	3brtr3d 5105	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑥𝐿𝐶))
69	1, 2, 32, 33, 8, 16, 12, 52, 19, 68	perprag 27087	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐵𝑥𝐶”⟩ ∈ (∟G‘𝐺))
70		trgcopy.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
71		trgcopy.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
72	1, 32, 33, 4, 20, 24, 70, 71	ncolne1 26986	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
73	72	necomd 2999	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ≠ 𝐷)
74	73	ad7antr 735	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ≠ 𝐷)
75	72	ad4antr 729	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ≠ 𝐸)
76	75	neneqd 2948	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐷 = 𝐸)
77	41	orcd 870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
78	1, 33, 32, 5, 10, 14, 42, 77	colrot2 26921	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝑥𝐿𝐴) ∨ 𝑥 = 𝐴))
79	1, 33, 32, 5, 42, 10, 14, 78	colcom 26919	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
80	79	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
81		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
82	1, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 80, 81	lnxfr 26927	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐸 ∈ (𝐷𝐿𝑦) ∨ 𝐷 = 𝑦))
83	1, 33, 32, 6, 22, 46, 26, 82	colrot2 26921	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
84	1, 33, 32, 6, 26, 22, 46, 83	colcom 26919	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
85	84	orcomd 868	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷 = 𝐸 ∨ 𝑦 ∈ (𝐷𝐿𝐸)))
86	85	ord 861	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (¬ 𝐷 = 𝐸 → 𝑦 ∈ (𝐷𝐿𝐸)))
87	76, 86	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ (𝐷𝐿𝐸))
88	87	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐷𝐿𝐸))
89	1, 32, 33, 8, 27, 23, 48, 74, 88	lncom 26983	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐸𝐿𝐷))
90		simprrr 779	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦 − 𝑓) = (𝑥 − 𝐶))
91	90	eqcomd 2744	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐶) = (𝑦 − 𝑓))
92	1, 2, 32, 8, 45, 19, 48, 28, 91, 65	tgcgrneq 26844	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑓)
93	1, 32, 33, 8, 48, 28, 92	tgelrnln 26991	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓) ∈ ran 𝐿)
94	1, 32, 33, 8, 27, 23, 74	tgelrnln 26991	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) ∈ ran 𝐿)
95		simpllr 773	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ∈ 𝑃)
96		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ∈ 𝑃)
97		simprl 768	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦))
98	33, 7, 97	perpln2 27072	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝑞𝐿𝑦) ∈ ran 𝐿)
99	1, 32, 33, 7, 96, 47, 98	tglnne 26989	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ≠ 𝑦)
100	99	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ≠ 𝑦)
101	100	necomd 2999	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑞)
102	1, 32, 33, 8, 48, 95, 101	tgelrnln 26991	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) ∈ ran 𝐿)
103	97	adantr 481	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦))
104	1, 32, 33, 8, 27, 23, 74	tglinecom 26996	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) = (𝐷𝐿𝐸))
105	1, 32, 33, 8, 48, 95, 101	tglinecom 26996	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) = (𝑞𝐿𝑦))
106	103, 104, 105	3brtr4d 5106	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑞))
107	1, 2, 32, 33, 8, 94, 102, 106	perpcom 27074	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞)(⟂G‘𝐺)(𝐸𝐿𝐷))
108		trgcopy.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (hlG‘𝐺)
109		simprrl 778	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓(𝐾‘𝑦)𝑞)
110	1, 32, 108, 28, 95, 48, 8, 33, 109	hlln 26968	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑞𝐿𝑦))
111	1, 32, 33, 8, 48, 95, 28, 101, 110	lncom 26983	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑦𝐿𝑞))
112	111	orcd 870	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑓 ∈ (𝑦𝐿𝑞) ∨ 𝑦 = 𝑞))
113	1, 2, 32, 33, 8, 48, 95, 28, 107, 112, 92	colperp 27090	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓)(⟂G‘𝐺)(𝐸𝐿𝐷))
114	1, 2, 32, 33, 8, 93, 94, 113	perpcom 27074	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑓))
115	1, 2, 32, 33, 8, 27, 23, 89, 28, 114	perprag 27087	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐸𝑦𝑓”⟩ ∈ (∟G‘𝐺))
116	81	ad3antrrr 727	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
117	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp2 26882	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝑥) = (𝐸 − 𝑦))
118	1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 115, 117, 91	hypcgr 27162	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝐶) = (𝐸 − 𝑓))
119		eqid 2738	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
120	51, 68	eqbrtrd 5096	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑥𝐿𝐶))
121	1, 2, 32, 33, 8, 12, 16, 49, 19, 120	perprag 27087	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝑥𝐶”⟩ ∈ (∟G‘𝐺))
122	1, 2, 32, 33, 119, 8, 12, 45, 19, 121	ragcom 27059	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐶𝑥𝐴”⟩ ∈ (∟G‘𝐺))
123	104, 114	eqbrtrrd 5098	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑦𝐿𝑓))
124	1, 2, 32, 33, 8, 23, 27, 88, 28, 123	perprag 27087	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐷𝑦𝑓”⟩ ∈ (∟G‘𝐺))
125	1, 2, 32, 33, 119, 8, 23, 48, 28, 124	ragcom 27059	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝑓𝑦𝐷”⟩ ∈ (∟G‘𝐺))
126	1, 2, 32, 8, 45, 19, 48, 28, 91	tgcgrcomlr 26841	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝑥) = (𝑓 − 𝑦))
127	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp3 26883	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐴) = (𝑦 − 𝐷))
128	1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 122, 125, 126, 127	hypcgr 27162	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝐴) = (𝑓 − 𝐷))
129	1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 118, 128	trgcgr 26877	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
130	1, 32, 33, 4, 20, 24, 72	tgelrnln 26991	. . . . . . . . 9 ⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿)
131	130	ad4antr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷𝐿𝐸) ∈ ran 𝐿)
132	131	ad3antrrr 727	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸) ∈ ran 𝐿)
133		simpl 483	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑤 = 𝑘)
134	133	eleq1d 2823	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
135		simpr 485	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑣 = 𝑙)
136	135	eleq1d 2823	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
137	134, 136	anbi12d 631	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ↔ (𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))))
138		simpr 485	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗)
139		simpll 764	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑤 = 𝑘)
140		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑣 = 𝑙)
141	139, 140	oveq12d 7293	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑤𝐼𝑣) = (𝑘𝐼𝑙))
142	138, 141	eleq12d 2833	. . . . . . . . . 10 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑧 ∈ (𝑤𝐼𝑣) ↔ 𝑗 ∈ (𝑘𝐼𝑙)))
143	142	cbvrexdva 3395	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣) ↔ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙)))
144	137, 143	anbi12d 631	. . . . . . . 8 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣)) ↔ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))))
145	144	cbvopabv 5147	. . . . . . 7 ⊢ {⟨𝑤, 𝑣⟩ ∣ ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣))} = {⟨𝑘, 𝑙⟩ ∣ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))}
146	8	adantr 481	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐺 ∈ TarskiG)
147	19	adantr 481	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐶 ∈ 𝑃)
148	16	adantr 481	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐵 ∈ 𝑃)
149	12	adantr 481	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐴 ∈ 𝑃)
150	23	adantr 481	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐷 ∈ 𝑃)
151	27	adantr 481	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ∈ 𝑃)
152	28	adantr 481	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ 𝑃)
153	73	ad8antr 737	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ≠ 𝐷)
154		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐷𝐿𝐸))
155	1, 32, 33, 146, 151, 150, 152, 153, 154	lncom 26983	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐸𝐿𝐷))
156	155	orcd 870	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝑓 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
157	1, 33, 32, 146, 151, 150, 152, 156	colrot1 26920	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐸 ∈ (𝐷𝐿𝑓) ∨ 𝐷 = 𝑓))
158	129	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
159	1, 2, 32, 3, 146, 149, 148, 147, 150, 151, 152, 158	trgcgrcom 26889	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐷𝐸𝑓”⟩(cgrG‘𝐺)⟨“𝐴𝐵𝐶”⟩)
160	1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159	lnxfr 26927	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
161	1, 33, 32, 146, 149, 147, 148, 160	colrot1 26920	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
162	1, 33, 32, 146, 147, 148, 149, 161	colcom 26919	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
163	34	ad8antr 737	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
164	162, 163	pm2.65da 814	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ¬ 𝑓 ∈ (𝐷𝐿𝐸))
165	1, 32, 33, 8, 132, 48, 145, 108, 88, 28, 95, 164, 109	hphl 27132	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞)
166	70	ad4antr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹 ∈ 𝑃)
167	166	ad2antrr 723	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐹 ∈ 𝑃)
168	167	adantr 481	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐹 ∈ 𝑃)
169		simplrr 775	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
170	1, 32, 33, 8, 132, 28, 145, 95, 165, 168, 169	hpgtr 27129	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
171	129, 170	jca 512	. . . . 5 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
172	1, 32, 108, 47, 44, 18, 7, 96, 2, 99, 64	hlcgrex 26977	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))
173	171, 172	reximddv 3204	. . . 4 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
174	1, 33, 32, 4, 24, 70, 20, 71	ncolrot2 26924	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
175		ioran 981	. . . . . . . 8 ⊢ (¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
176	174, 175	sylib 217	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
177	176	simpld 495	. . . . . 6 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
178	177	ad4antr 729	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
179	1, 2, 32, 33, 6, 36, 131, 145, 87, 166, 178	lnperpex 27164	. . . 4 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑞 ∈ 𝑃 ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
180	173, 179	r19.29a 3218	. . 3 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
181	1, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 79, 30	lnext 26928	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑦 ∈ 𝑃 ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
182	180, 181	r19.29a 3218	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
183	1, 2, 32, 33, 4, 39, 17, 60	footex 27082	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴𝐿𝐵)(𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
184	182, 183	r19.29a 3218	1 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∨ wo 844 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 ∖ cdif 3884 class class class wbr 5074 {copab 5136 ran crn 5590 ‘cfv 6433 (class class class)co 7275 2c2 12028 ⟨“cs3 14555 Basecbs 16912 distcds 16971 TarskiGcstrkg 26788 Dim_TarskiG≥cstrkgld 26792 Itvcitv 26794 LineGclng 26795 cgrGccgrg 26871 hlGchlg 26961 pInvGcmir 27013 ⟂Gcperpg 27056 hpGchpg 27118

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4840 df-int 4880 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-1o 8297 df-oadd 8301 df-er 8498 df-map 8617 df-pm 8618 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-dju 9659 df-card 9697 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-nn 11974 df-2 12036 df-3 12037 df-n0 12234 df-xnn0 12306 df-z 12320 df-uz 12583 df-fz 13240 df-fzo 13383 df-hash 14045 df-word 14218 df-concat 14274 df-s1 14301 df-s2 14561 df-s3 14562 df-trkgc 26809 df-trkgb 26810 df-trkgcb 26811 df-trkgld 26813 df-trkg 26814 df-cgrg 26872 df-ismt 26894 df-leg 26944 df-hlg 26962 df-mir 27014 df-rag 27055 df-perpg 27057 df-hpg 27119 df-mid 27135 df-lmi 27136

This theorem is referenced by: trgcopyeu 27167 acopy 27194 cgrg3col4 27214

W3C validator