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 28886

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 2737	. . . . . . 7 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
4		trgcopy.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
6	5	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
7	6	ad2antrr 727	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐺 ∈ TarskiG)
8	7	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺 ∈ TarskiG)
9		trgcopy.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10	9	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
11	10	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴 ∈ 𝑃)
12	11	ad3antrrr 731	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ∈ 𝑃)
13		trgcopy.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
14	13	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
15	14	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵 ∈ 𝑃)
16	15	ad3antrrr 731	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐵 ∈ 𝑃)
17		trgcopy.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
18	17	ad6antr 737	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐶 ∈ 𝑃)
19	18	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ∈ 𝑃)
20		trgcopy.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
21	20	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐷 ∈ 𝑃)
22	21	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ∈ 𝑃)
23	22	ad3antrrr 731	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐷 ∈ 𝑃)
24		trgcopy.e	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
25	24	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐸 ∈ 𝑃)
26	25	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸 ∈ 𝑃)
27	26	ad3antrrr 731	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ∈ 𝑃)
28		simprl 771	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ 𝑃)
29		trgcopy.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))
30	29	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
31	30	ad5antr 735	. . . . . . 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 28647	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
36	35	ad4antr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺Dim_TarskiG≥2)
37	36	ad3antrrr 731	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺Dim_TarskiG≥2)
38	1, 32, 33, 4, 9, 13, 17, 34	ncolne1 28707	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	1, 32, 33, 4, 9, 13, 38	tgelrnln 28712	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
40	39	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴𝐿𝐵) ∈ ran 𝐿)
41		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ (𝐴𝐿𝐵))
42	1, 33, 32, 5, 40, 41	tglnpt 28631	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ 𝑃)
43	42	ad2antrr 727	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑥 ∈ 𝑃)
44	43	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ∈ 𝑃)
45	44	adantr 480	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ 𝑃)
46		simplr 769	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ 𝑃)
47	46	ad2antrr 727	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑦 ∈ 𝑃)
48	47	adantr 480	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ 𝑃)
49	41	ad5antr 735	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐴𝐿𝐵))
50	38	ad7antr 739	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ≠ 𝐵)
51	1, 32, 33, 8, 12, 16, 50	tglinecom 28717	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
52	49, 51	eleqtrd 2839	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐵𝐿𝐴))
53		simp-6r 788	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
54	33, 8, 53	perpln1 28792	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
55	40	ad5antr 735	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) ∈ ran 𝐿)
56	1, 2, 32, 33, 8, 54, 55, 53	perpcom 28795	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝑥))
57	1, 33, 32, 4, 13, 17, 9, 34	ncolrot2 28645	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
58		ioran 986	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ↔ (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
59	57, 58	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
60	59	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
61	60	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
62		nelne2 3031	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐶 ∈ (𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
63	41, 61, 62	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
64	63	ad4antr 733	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ≠ 𝐶)
65	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ≠ 𝐶)
66	65	necomd 2988	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ≠ 𝑥)
67	1, 32, 33, 8, 19, 45, 66	tglinecom 28717	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) = (𝑥𝐿𝐶))
68	56, 51, 67	3brtr3d 5117	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑥𝐿𝐶))
69	1, 2, 32, 33, 8, 16, 12, 52, 19, 68	perprag 28808	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐵𝑥𝐶”⟩ ∈ (∟G‘𝐺))
70		trgcopy.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
71		trgcopy.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
72	1, 32, 33, 4, 20, 24, 70, 71	ncolne1 28707	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
73	72	necomd 2988	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ≠ 𝐷)
74	73	ad7antr 739	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ≠ 𝐷)
75	72	ad4antr 733	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ≠ 𝐸)
76	75	neneqd 2938	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐷 = 𝐸)
77	41	orcd 874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
78	1, 33, 32, 5, 10, 14, 42, 77	colrot2 28642	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝑥𝐿𝐴) ∨ 𝑥 = 𝐴))
79	1, 33, 32, 5, 42, 10, 14, 78	colcom 28640	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
80	79	ad2antrr 727	. . . . . . . . . . . . . . . . 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 28648	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐸 ∈ (𝐷𝐿𝑦) ∨ 𝐷 = 𝑦))
83	1, 33, 32, 6, 22, 46, 26, 82	colrot2 28642	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
84	1, 33, 32, 6, 26, 22, 46, 83	colcom 28640	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
85	84	orcomd 872	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷 = 𝐸 ∨ 𝑦 ∈ (𝐷𝐿𝐸)))
86	85	ord 865	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (¬ 𝐷 = 𝐸 → 𝑦 ∈ (𝐷𝐿𝐸)))
87	76, 86	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ (𝐷𝐿𝐸))
88	87	ad3antrrr 731	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐷𝐿𝐸))
89	1, 32, 33, 8, 27, 23, 48, 74, 88	lncom 28704	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐸𝐿𝐷))
90		simprrr 782	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦 − 𝑓) = (𝑥 − 𝐶))
91	90	eqcomd 2743	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐶) = (𝑦 − 𝑓))
92	1, 2, 32, 8, 45, 19, 48, 28, 91, 65	tgcgrneq 28565	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑓)
93	1, 32, 33, 8, 48, 28, 92	tgelrnln 28712	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓) ∈ ran 𝐿)
94	1, 32, 33, 8, 27, 23, 74	tgelrnln 28712	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) ∈ ran 𝐿)
95		simpllr 776	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ∈ 𝑃)
96		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ∈ 𝑃)
97		simprl 771	. . . . . . . . . . . . . . . . 17 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦))
98	33, 7, 97	perpln2 28793	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝑞𝐿𝑦) ∈ ran 𝐿)
99	1, 32, 33, 7, 96, 47, 98	tglnne 28710	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ≠ 𝑦)
100	99	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ≠ 𝑦)
101	100	necomd 2988	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑞)
102	1, 32, 33, 8, 48, 95, 101	tgelrnln 28712	. . . . . . . . . . . 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 28717	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) = (𝐷𝐿𝐸))
105	1, 32, 33, 8, 48, 95, 101	tglinecom 28717	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) = (𝑞𝐿𝑦))
106	103, 104, 105	3brtr4d 5118	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑞))
107	1, 2, 32, 33, 8, 94, 102, 106	perpcom 28795	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞)(⟂G‘𝐺)(𝐸𝐿𝐷))
108		trgcopy.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (hlG‘𝐺)
109		simprrl 781	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓(𝐾‘𝑦)𝑞)
110	1, 32, 108, 28, 95, 48, 8, 33, 109	hlln 28689	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑞𝐿𝑦))
111	1, 32, 33, 8, 48, 95, 28, 101, 110	lncom 28704	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑦𝐿𝑞))
112	111	orcd 874	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑓 ∈ (𝑦𝐿𝑞) ∨ 𝑦 = 𝑞))
113	1, 2, 32, 33, 8, 48, 95, 28, 107, 112, 92	colperp 28811	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓)(⟂G‘𝐺)(𝐸𝐿𝐷))
114	1, 2, 32, 33, 8, 93, 94, 113	perpcom 28795	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑓))
115	1, 2, 32, 33, 8, 27, 23, 89, 28, 114	perprag 28808	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐸𝑦𝑓”⟩ ∈ (∟G‘𝐺))
116	81	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
117	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp2 28603	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝑥) = (𝐸 − 𝑦))
118	1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 115, 117, 91	hypcgr 28883	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝐶) = (𝐸 − 𝑓))
119		eqid 2737	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
120	51, 68	eqbrtrd 5108	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑥𝐿𝐶))
121	1, 2, 32, 33, 8, 12, 16, 49, 19, 120	perprag 28808	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝑥𝐶”⟩ ∈ (∟G‘𝐺))
122	1, 2, 32, 33, 119, 8, 12, 45, 19, 121	ragcom 28780	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐶𝑥𝐴”⟩ ∈ (∟G‘𝐺))
123	104, 114	eqbrtrrd 5110	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑦𝐿𝑓))
124	1, 2, 32, 33, 8, 23, 27, 88, 28, 123	perprag 28808	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐷𝑦𝑓”⟩ ∈ (∟G‘𝐺))
125	1, 2, 32, 33, 119, 8, 23, 48, 28, 124	ragcom 28780	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝑓𝑦𝐷”⟩ ∈ (∟G‘𝐺))
126	1, 2, 32, 8, 45, 19, 48, 28, 91	tgcgrcomlr 28562	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝑥) = (𝑓 − 𝑦))
127	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp3 28604	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐴) = (𝑦 − 𝐷))
128	1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 122, 125, 126, 127	hypcgr 28883	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝐴) = (𝑓 − 𝐷))
129	1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 118, 128	trgcgr 28598	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
130	1, 32, 33, 4, 20, 24, 72	tgelrnln 28712	. . . . . . . . 9 ⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿)
131	130	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷𝐿𝐸) ∈ ran 𝐿)
132	131	ad3antrrr 731	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸) ∈ ran 𝐿)
133		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑤 = 𝑘)
134	133	eleq1d 2822	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
135		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑣 = 𝑙)
136	135	eleq1d 2822	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
137	134, 136	anbi12d 633	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ↔ (𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))))
138		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗)
139		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑤 = 𝑘)
140		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑣 = 𝑙)
141	139, 140	oveq12d 7378	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑤𝐼𝑣) = (𝑘𝐼𝑙))
142	138, 141	eleq12d 2831	. . . . . . . . . 10 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑧 ∈ (𝑤𝐼𝑣) ↔ 𝑗 ∈ (𝑘𝐼𝑙)))
143	142	cbvrexdva 3219	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣) ↔ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙)))
144	137, 143	anbi12d 633	. . . . . . . 8 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣)) ↔ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))))
145	144	cbvopabv 5159	. . . . . . 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 741	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ≠ 𝐷)
154		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐷𝐿𝐸))
155	1, 32, 33, 146, 151, 150, 152, 153, 154	lncom 28704	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐸𝐿𝐷))
156	155	orcd 874	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝑓 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
157	1, 33, 32, 146, 151, 150, 152, 156	colrot1 28641	. . . . . . . . . . . 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 28610	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐷𝐸𝑓”⟩(cgrG‘𝐺)⟨“𝐴𝐵𝐶”⟩)
160	1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159	lnxfr 28648	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
161	1, 33, 32, 146, 149, 147, 148, 160	colrot1 28641	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
162	1, 33, 32, 146, 147, 148, 149, 161	colcom 28640	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
163	34	ad8antr 741	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
164	162, 163	pm2.65da 817	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ¬ 𝑓 ∈ (𝐷𝐿𝐸))
165	1, 32, 33, 8, 132, 48, 145, 108, 88, 28, 95, 164, 109	hphl 28853	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞)
166	70	ad4antr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹 ∈ 𝑃)
167	166	ad2antrr 727	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐹 ∈ 𝑃)
168	167	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐹 ∈ 𝑃)
169		simplrr 778	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
170	1, 32, 33, 8, 132, 28, 145, 95, 165, 168, 169	hpgtr 28850	. . . . . 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 28698	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))
173	171, 172	reximddv 3154	. . . 4 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
174	1, 33, 32, 4, 24, 70, 20, 71	ncolrot2 28645	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
175		ioran 986	. . . . . . . 8 ⊢ (¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
176	174, 175	sylib 218	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
177	176	simpld 494	. . . . . 6 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
178	177	ad4antr 733	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
179	1, 2, 32, 33, 6, 36, 131, 145, 87, 166, 178	lnperpex 28885	. . . 4 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑞 ∈ 𝑃 ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
180	173, 179	r19.29a 3146	. . 3 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
181	1, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 79, 30	lnext 28649	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑦 ∈ 𝑃 ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
182	180, 181	r19.29a 3146	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
183	1, 2, 32, 33, 4, 39, 17, 60	footex 28803	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴𝐿𝐵)(𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
184	182, 183	r19.29a 3146	1 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 ∖ cdif 3887 class class class wbr 5086 {copab 5148 ran crn 5625 ‘cfv 6492 (class class class)co 7360 2c2 12227 ⟨“cs3 14795 Basecbs 17170 distcds 17220 TarskiGcstrkg 28509 Dim_TarskiG≥cstrkgld 28513 Itvcitv 28515 LineGclng 28516 cgrGccgrg 28592 hlGchlg 28682 pInvGcmir 28734 ⟂Gcperpg 28777 hpGchpg 28839

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-oadd 8402 df-er 8636 df-map 8768 df-pm 8769 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-fz 13453 df-fzo 13600 df-hash 14284 df-word 14467 df-concat 14524 df-s1 14550 df-s2 14801 df-s3 14802 df-trkgc 28530 df-trkgb 28531 df-trkgcb 28532 df-trkgld 28534 df-trkg 28535 df-cgrg 28593 df-ismt 28615 df-leg 28665 df-hlg 28683 df-mir 28735 df-rag 28776 df-perpg 28778 df-hpg 28840 df-mid 28856 df-lmi 28857

This theorem is referenced by: trgcopyeu 28888 acopy 28915 cgrg3col4 28935

W3C validator