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 28830

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 2740	. . . . . . 7 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
4		trgcopy.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
6	5	ad2antrr 725	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
7	6	ad2antrr 725	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐺 ∈ TarskiG)
8	7	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺 ∈ TarskiG)
9		trgcopy.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10	9	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
11	10	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴 ∈ 𝑃)
12	11	ad3antrrr 729	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ∈ 𝑃)
13		trgcopy.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
14	13	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
15	14	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵 ∈ 𝑃)
16	15	ad3antrrr 729	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐵 ∈ 𝑃)
17		trgcopy.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
18	17	ad6antr 735	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐶 ∈ 𝑃)
19	18	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ∈ 𝑃)
20		trgcopy.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
21	20	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐷 ∈ 𝑃)
22	21	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ∈ 𝑃)
23	22	ad3antrrr 729	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐷 ∈ 𝑃)
24		trgcopy.e	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
25	24	ad2antrr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐸 ∈ 𝑃)
26	25	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸 ∈ 𝑃)
27	26	ad3antrrr 729	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ∈ 𝑃)
28		simprl 770	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ 𝑃)
29		trgcopy.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))
30	29	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
31	30	ad5antr 733	. . . . . . 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 28591	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
36	35	ad4antr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺Dim_TarskiG≥2)
37	36	ad3antrrr 729	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺Dim_TarskiG≥2)
38	1, 32, 33, 4, 9, 13, 17, 34	ncolne1 28651	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	1, 32, 33, 4, 9, 13, 38	tgelrnln 28656	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
40	39	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴𝐿𝐵) ∈ ran 𝐿)
41		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ (𝐴𝐿𝐵))
42	1, 33, 32, 5, 40, 41	tglnpt 28575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ 𝑃)
43	42	ad2antrr 725	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑥 ∈ 𝑃)
44	43	ad2antrr 725	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ∈ 𝑃)
45	44	adantr 480	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ 𝑃)
46		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ 𝑃)
47	46	ad2antrr 725	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑦 ∈ 𝑃)
48	47	adantr 480	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ 𝑃)
49	41	ad5antr 733	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐴𝐿𝐵))
50	38	ad7antr 737	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ≠ 𝐵)
51	1, 32, 33, 8, 12, 16, 50	tglinecom 28661	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
52	49, 51	eleqtrd 2846	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐵𝐿𝐴))
53		simp-6r 787	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
54	33, 8, 53	perpln1 28736	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
55	40	ad5antr 733	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) ∈ ran 𝐿)
56	1, 2, 32, 33, 8, 54, 55, 53	perpcom 28739	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝑥))
57	1, 33, 32, 4, 13, 17, 9, 34	ncolrot2 28589	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
58		ioran 984	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ↔ (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
59	57, 58	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
60	59	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
61	60	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
62		nelne2 3046	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐶 ∈ (𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
63	41, 61, 62	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
64	63	ad4antr 731	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ≠ 𝐶)
65	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ≠ 𝐶)
66	65	necomd 3002	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ≠ 𝑥)
67	1, 32, 33, 8, 19, 45, 66	tglinecom 28661	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) = (𝑥𝐿𝐶))
68	56, 51, 67	3brtr3d 5197	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑥𝐿𝐶))
69	1, 2, 32, 33, 8, 16, 12, 52, 19, 68	perprag 28752	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐵𝑥𝐶”⟩ ∈ (∟G‘𝐺))
70		trgcopy.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
71		trgcopy.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
72	1, 32, 33, 4, 20, 24, 70, 71	ncolne1 28651	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
73	72	necomd 3002	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ≠ 𝐷)
74	73	ad7antr 737	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ≠ 𝐷)
75	72	ad4antr 731	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ≠ 𝐸)
76	75	neneqd 2951	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐷 = 𝐸)
77	41	orcd 872	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
78	1, 33, 32, 5, 10, 14, 42, 77	colrot2 28586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝑥𝐿𝐴) ∨ 𝑥 = 𝐴))
79	1, 33, 32, 5, 42, 10, 14, 78	colcom 28584	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
80	79	ad2antrr 725	. . . . . . . . . . . . . . . . 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 28592	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐸 ∈ (𝐷𝐿𝑦) ∨ 𝐷 = 𝑦))
83	1, 33, 32, 6, 22, 46, 26, 82	colrot2 28586	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
84	1, 33, 32, 6, 26, 22, 46, 83	colcom 28584	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
85	84	orcomd 870	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷 = 𝐸 ∨ 𝑦 ∈ (𝐷𝐿𝐸)))
86	85	ord 863	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (¬ 𝐷 = 𝐸 → 𝑦 ∈ (𝐷𝐿𝐸)))
87	76, 86	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ (𝐷𝐿𝐸))
88	87	ad3antrrr 729	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐷𝐿𝐸))
89	1, 32, 33, 8, 27, 23, 48, 74, 88	lncom 28648	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐸𝐿𝐷))
90		simprrr 781	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦 − 𝑓) = (𝑥 − 𝐶))
91	90	eqcomd 2746	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐶) = (𝑦 − 𝑓))
92	1, 2, 32, 8, 45, 19, 48, 28, 91, 65	tgcgrneq 28509	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑓)
93	1, 32, 33, 8, 48, 28, 92	tgelrnln 28656	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓) ∈ ran 𝐿)
94	1, 32, 33, 8, 27, 23, 74	tgelrnln 28656	. . . . . . . . . 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 28737	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝑞𝐿𝑦) ∈ ran 𝐿)
99	1, 32, 33, 7, 96, 47, 98	tglnne 28654	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ≠ 𝑦)
100	99	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ≠ 𝑦)
101	100	necomd 3002	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑞)
102	1, 32, 33, 8, 48, 95, 101	tgelrnln 28656	. . . . . . . . . . . 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 28661	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) = (𝐷𝐿𝐸))
105	1, 32, 33, 8, 48, 95, 101	tglinecom 28661	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) = (𝑞𝐿𝑦))
106	103, 104, 105	3brtr4d 5198	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑞))
107	1, 2, 32, 33, 8, 94, 102, 106	perpcom 28739	. . . . . . . . . . 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 28633	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑞𝐿𝑦))
111	1, 32, 33, 8, 48, 95, 28, 101, 110	lncom 28648	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑦𝐿𝑞))
112	111	orcd 872	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑓 ∈ (𝑦𝐿𝑞) ∨ 𝑦 = 𝑞))
113	1, 2, 32, 33, 8, 48, 95, 28, 107, 112, 92	colperp 28755	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓)(⟂G‘𝐺)(𝐸𝐿𝐷))
114	1, 2, 32, 33, 8, 93, 94, 113	perpcom 28739	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑓))
115	1, 2, 32, 33, 8, 27, 23, 89, 28, 114	perprag 28752	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐸𝑦𝑓”⟩ ∈ (∟G‘𝐺))
116	81	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
117	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp2 28547	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝑥) = (𝐸 − 𝑦))
118	1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 115, 117, 91	hypcgr 28827	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝐶) = (𝐸 − 𝑓))
119		eqid 2740	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
120	51, 68	eqbrtrd 5188	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑥𝐿𝐶))
121	1, 2, 32, 33, 8, 12, 16, 49, 19, 120	perprag 28752	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝑥𝐶”⟩ ∈ (∟G‘𝐺))
122	1, 2, 32, 33, 119, 8, 12, 45, 19, 121	ragcom 28724	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐶𝑥𝐴”⟩ ∈ (∟G‘𝐺))
123	104, 114	eqbrtrrd 5190	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑦𝐿𝑓))
124	1, 2, 32, 33, 8, 23, 27, 88, 28, 123	perprag 28752	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐷𝑦𝑓”⟩ ∈ (∟G‘𝐺))
125	1, 2, 32, 33, 119, 8, 23, 48, 28, 124	ragcom 28724	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝑓𝑦𝐷”⟩ ∈ (∟G‘𝐺))
126	1, 2, 32, 8, 45, 19, 48, 28, 91	tgcgrcomlr 28506	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝑥) = (𝑓 − 𝑦))
127	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp3 28548	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐴) = (𝑦 − 𝐷))
128	1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 122, 125, 126, 127	hypcgr 28827	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝐴) = (𝑓 − 𝐷))
129	1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 118, 128	trgcgr 28542	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
130	1, 32, 33, 4, 20, 24, 72	tgelrnln 28656	. . . . . . . . 9 ⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿)
131	130	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷𝐿𝐸) ∈ ran 𝐿)
132	131	ad3antrrr 729	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸) ∈ ran 𝐿)
133		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑤 = 𝑘)
134	133	eleq1d 2829	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
135		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑣 = 𝑙)
136	135	eleq1d 2829	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
137	134, 136	anbi12d 631	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ↔ (𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))))
138		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗)
139		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑤 = 𝑘)
140		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑣 = 𝑙)
141	139, 140	oveq12d 7466	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑤𝐼𝑣) = (𝑘𝐼𝑙))
142	138, 141	eleq12d 2838	. . . . . . . . . 10 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑧 ∈ (𝑤𝐼𝑣) ↔ 𝑗 ∈ (𝑘𝐼𝑙)))
143	142	cbvrexdva 3246	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣) ↔ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙)))
144	137, 143	anbi12d 631	. . . . . . . 8 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣)) ↔ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))))
145	144	cbvopabv 5239	. . . . . . 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 739	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ≠ 𝐷)
154		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐷𝐿𝐸))
155	1, 32, 33, 146, 151, 150, 152, 153, 154	lncom 28648	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐸𝐿𝐷))
156	155	orcd 872	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝑓 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
157	1, 33, 32, 146, 151, 150, 152, 156	colrot1 28585	. . . . . . . . . . . 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 28554	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐷𝐸𝑓”⟩(cgrG‘𝐺)⟨“𝐴𝐵𝐶”⟩)
160	1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159	lnxfr 28592	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
161	1, 33, 32, 146, 149, 147, 148, 160	colrot1 28585	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
162	1, 33, 32, 146, 147, 148, 149, 161	colcom 28584	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
163	34	ad8antr 739	. . . . . . . . 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 28797	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞)
166	70	ad4antr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹 ∈ 𝑃)
167	166	ad2antrr 725	. . . . . . . 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 28794	. . . . . 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 28642	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))
173	171, 172	reximddv 3177	. . . 4 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
174	1, 33, 32, 4, 24, 70, 20, 71	ncolrot2 28589	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
175		ioran 984	. . . . . . . 8 ⊢ (¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
176	174, 175	sylib 218	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
177	176	simpld 494	. . . . . 6 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
178	177	ad4antr 731	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
179	1, 2, 32, 33, 6, 36, 131, 145, 87, 166, 178	lnperpex 28829	. . . 4 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑞 ∈ 𝑃 ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
180	173, 179	r19.29a 3168	. . 3 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
181	1, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 79, 30	lnext 28593	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑦 ∈ 𝑃 ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
182	180, 181	r19.29a 3168	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
183	1, 2, 32, 33, 4, 39, 17, 60	footex 28747	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴𝐿𝐵)(𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
184	182, 183	r19.29a 3168	1 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 846 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ∃wrex 3076 ∖ cdif 3973 class class class wbr 5166 {copab 5228 ran crn 5701 ‘cfv 6573 (class class class)co 7448 2c2 12348 ⟨“cs3 14891 Basecbs 17258 distcds 17320 TarskiGcstrkg 28453 Dim_TarskiG≥cstrkgld 28457 Itvcitv 28459 LineGclng 28460 cgrGccgrg 28536 hlGchlg 28626 pInvGcmir 28678 ⟂Gcperpg 28721 hpGchpg 28783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-oadd 8526 df-er 8763 df-map 8886 df-pm 8887 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-dju 9970 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-xnn0 12626 df-z 12640 df-uz 12904 df-fz 13568 df-fzo 13712 df-hash 14380 df-word 14563 df-concat 14619 df-s1 14644 df-s2 14897 df-s3 14898 df-trkgc 28474 df-trkgb 28475 df-trkgcb 28476 df-trkgld 28478 df-trkg 28479 df-cgrg 28537 df-ismt 28559 df-leg 28609 df-hlg 28627 df-mir 28679 df-rag 28720 df-perpg 28722 df-hpg 28784 df-mid 28800 df-lmi 28801

This theorem is referenced by: trgcopyeu 28832 acopy 28859 cgrg3col4 28879

W3C validator