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 28731

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 2729	. . . . . . 7 ⊢ (cgrG‘𝐺) = (cgrG‘𝐺)
4		trgcopy.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐺 ∈ TarskiG)
6	5	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺 ∈ TarskiG)
7	6	ad2antrr 726	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐺 ∈ TarskiG)
8	7	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺 ∈ TarskiG)
9		trgcopy.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
10	9	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐴 ∈ 𝑃)
11	10	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐴 ∈ 𝑃)
12	11	ad3antrrr 730	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ∈ 𝑃)
13		trgcopy.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
14	13	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐵 ∈ 𝑃)
15	14	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐵 ∈ 𝑃)
16	15	ad3antrrr 730	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐵 ∈ 𝑃)
17		trgcopy.c	. . . . . . . . 9 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
18	17	ad6antr 736	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐶 ∈ 𝑃)
19	18	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ∈ 𝑃)
20		trgcopy.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
21	20	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐷 ∈ 𝑃)
22	21	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ∈ 𝑃)
23	22	ad3antrrr 730	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐷 ∈ 𝑃)
24		trgcopy.e	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
25	24	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝐸 ∈ 𝑃)
26	25	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐸 ∈ 𝑃)
27	26	ad3antrrr 730	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ∈ 𝑃)
28		simprl 770	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ 𝑃)
29		trgcopy.3	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐷 − 𝐸))
30	29	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
31	30	ad5antr 734	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴 − 𝐵) = (𝐷 − 𝐸))
32		trgcopy.i	. . . . . . . 8 ⊢ 𝐼 = (Itv‘𝐺)
33		trgcopy.l	. . . . . . . . . . 11 ⊢ 𝐿 = (LineG‘𝐺)
34		trgcopy.1	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
35	1, 33, 32, 4, 13, 17, 9, 34	ncoltgdim2 28492	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
36	35	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐺Dim_TarskiG≥2)
37	36	ad3antrrr 730	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐺Dim_TarskiG≥2)
38	1, 32, 33, 4, 9, 13, 17, 34	ncolne1 28552	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	1, 32, 33, 4, 9, 13, 38	tgelrnln 28557	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴𝐿𝐵) ∈ ran 𝐿)
40	39	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐴𝐿𝐵) ∈ ran 𝐿)
41		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ (𝐴𝐿𝐵))
42	1, 33, 32, 5, 40, 41	tglnpt 28476	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ∈ 𝑃)
43	42	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑥 ∈ 𝑃)
44	43	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ∈ 𝑃)
45	44	adantr 480	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ 𝑃)
46		simplr 768	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ 𝑃)
47	46	ad2antrr 726	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑦 ∈ 𝑃)
48	47	adantr 480	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ 𝑃)
49	41	ad5antr 734	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐴𝐿𝐵))
50	38	ad7antr 738	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐴 ≠ 𝐵)
51	1, 32, 33, 8, 12, 16, 50	tglinecom 28562	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) = (𝐵𝐿𝐴))
52	49, 51	eleqtrd 2830	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ∈ (𝐵𝐿𝐴))
53		simp-6r 787	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
54	33, 8, 53	perpln1 28637	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
55	40	ad5antr 734	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵) ∈ ran 𝐿)
56	1, 2, 32, 33, 8, 54, 55, 53	perpcom 28640	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝐶𝐿𝑥))
57	1, 33, 32, 4, 13, 17, 9, 34	ncolrot2 28490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
58		ioran 985	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵) ↔ (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
59	57, 58	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (¬ 𝐶 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐴 = 𝐵))
60	59	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
61	60	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ¬ 𝐶 ∈ (𝐴𝐿𝐵))
62		nelne2 3023	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (𝐴𝐿𝐵) ∧ ¬ 𝐶 ∈ (𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
63	41, 61, 62	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → 𝑥 ≠ 𝐶)
64	63	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑥 ≠ 𝐶)
65	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑥 ≠ 𝐶)
66	65	necomd 2980	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐶 ≠ 𝑥)
67	1, 32, 33, 8, 19, 45, 66	tglinecom 28562	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶𝐿𝑥) = (𝑥𝐿𝐶))
68	56, 51, 67	3brtr3d 5138	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵𝐿𝐴)(⟂G‘𝐺)(𝑥𝐿𝐶))
69	1, 2, 32, 33, 8, 16, 12, 52, 19, 68	perprag 28653	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐵𝑥𝐶”⟩ ∈ (∟G‘𝐺))
70		trgcopy.f	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
71		trgcopy.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ (𝐷 ∈ (𝐸𝐿𝐹) ∨ 𝐸 = 𝐹))
72	1, 32, 33, 4, 20, 24, 70, 71	ncolne1 28552	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐷 ≠ 𝐸)
73	72	necomd 2980	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ≠ 𝐷)
74	73	ad7antr 738	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐸 ≠ 𝐷)
75	72	ad4antr 732	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐷 ≠ 𝐸)
76	75	neneqd 2930	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐷 = 𝐸)
77	41	orcd 873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝑥 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
78	1, 33, 32, 5, 10, 14, 42, 77	colrot2 28487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝑥𝐿𝐴) ∨ 𝑥 = 𝐴))
79	1, 33, 32, 5, 42, 10, 14, 78	colcom 28485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
80	79	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐵 ∈ (𝐴𝐿𝑥) ∨ 𝐴 = 𝑥))
81		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
82	1, 33, 32, 6, 11, 15, 43, 3, 22, 26, 46, 80, 81	lnxfr 28493	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐸 ∈ (𝐷𝐿𝑦) ∨ 𝐷 = 𝑦))
83	1, 33, 32, 6, 22, 46, 26, 82	colrot2 28487	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
84	1, 33, 32, 6, 26, 22, 46, 83	colcom 28485	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝑦 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
85	84	orcomd 871	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷 = 𝐸 ∨ 𝑦 ∈ (𝐷𝐿𝐸)))
86	85	ord 864	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (¬ 𝐷 = 𝐸 → 𝑦 ∈ (𝐷𝐿𝐸)))
87	76, 86	mpd 15	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝑦 ∈ (𝐷𝐿𝐸))
88	87	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐷𝐿𝐸))
89	1, 32, 33, 8, 27, 23, 48, 74, 88	lncom 28549	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ∈ (𝐸𝐿𝐷))
90		simprrr 781	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦 − 𝑓) = (𝑥 − 𝐶))
91	90	eqcomd 2735	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐶) = (𝑦 − 𝑓))
92	1, 2, 32, 8, 45, 19, 48, 28, 91, 65	tgcgrneq 28410	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑓)
93	1, 32, 33, 8, 48, 28, 92	tgelrnln 28557	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓) ∈ ran 𝐿)
94	1, 32, 33, 8, 27, 23, 74	tgelrnln 28557	. . . . . . . . . 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 28638	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → (𝑞𝐿𝑦) ∈ ran 𝐿)
99	1, 32, 33, 7, 96, 47, 98	tglnne 28555	. . . . . . . . . . . . . . 15 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝑞 ≠ 𝑦)
100	99	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞 ≠ 𝑦)
101	100	necomd 2980	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑦 ≠ 𝑞)
102	1, 32, 33, 8, 48, 95, 101	tgelrnln 28557	. . . . . . . . . . . 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 28562	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷) = (𝐷𝐿𝐸))
105	1, 32, 33, 8, 48, 95, 101	tglinecom 28562	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑞) = (𝑞𝐿𝑦))
106	103, 104, 105	3brtr4d 5139	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑞))
107	1, 2, 32, 33, 8, 94, 102, 106	perpcom 28640	. . . . . . . . . . 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 28534	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑞𝐿𝑦))
111	1, 32, 33, 8, 48, 95, 28, 101, 110	lncom 28549	. . . . . . . . . . . 12 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓 ∈ (𝑦𝐿𝑞))
112	111	orcd 873	. . . . . . . . . . 11 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑓 ∈ (𝑦𝐿𝑞) ∨ 𝑦 = 𝑞))
113	1, 2, 32, 33, 8, 48, 95, 28, 107, 112, 92	colperp 28656	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑦𝐿𝑓)(⟂G‘𝐺)(𝐸𝐿𝐷))
114	1, 2, 32, 33, 8, 93, 94, 113	perpcom 28640	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐸𝐿𝐷)(⟂G‘𝐺)(𝑦𝐿𝑓))
115	1, 2, 32, 33, 8, 27, 23, 89, 28, 114	perprag 28653	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐸𝑦𝑓”⟩ ∈ (∟G‘𝐺))
116	81	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
117	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp2 28448	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝑥) = (𝐸 − 𝑦))
118	1, 2, 32, 8, 37, 16, 45, 19, 27, 48, 28, 69, 115, 117, 91	hypcgr 28728	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐵 − 𝐶) = (𝐸 − 𝑓))
119		eqid 2729	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
120	51, 68	eqbrtrd 5129	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐴𝐿𝐵)(⟂G‘𝐺)(𝑥𝐿𝐶))
121	1, 2, 32, 33, 8, 12, 16, 49, 19, 120	perprag 28653	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝑥𝐶”⟩ ∈ (∟G‘𝐺))
122	1, 2, 32, 33, 119, 8, 12, 45, 19, 121	ragcom 28625	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐶𝑥𝐴”⟩ ∈ (∟G‘𝐺))
123	104, 114	eqbrtrrd 5131	. . . . . . . . . 10 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸)(⟂G‘𝐺)(𝑦𝐿𝑓))
124	1, 2, 32, 33, 8, 23, 27, 88, 28, 123	perprag 28653	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐷𝑦𝑓”⟩ ∈ (∟G‘𝐺))
125	1, 2, 32, 33, 119, 8, 23, 48, 28, 124	ragcom 28625	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝑓𝑦𝐷”⟩ ∈ (∟G‘𝐺))
126	1, 2, 32, 8, 45, 19, 48, 28, 91	tgcgrcomlr 28407	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝑥) = (𝑓 − 𝑦))
127	1, 2, 32, 3, 8, 12, 16, 45, 23, 27, 48, 116	cgr3simp3 28449	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝑥 − 𝐴) = (𝑦 − 𝐷))
128	1, 2, 32, 8, 37, 19, 45, 12, 28, 48, 23, 122, 125, 126, 127	hypcgr 28728	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐶 − 𝐴) = (𝑓 − 𝐷))
129	1, 2, 3, 8, 12, 16, 19, 23, 27, 28, 31, 118, 128	trgcgr 28443	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩)
130	1, 32, 33, 4, 20, 24, 72	tgelrnln 28557	. . . . . . . . 9 ⊢ (𝜑 → (𝐷𝐿𝐸) ∈ ran 𝐿)
131	130	ad4antr 732	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → (𝐷𝐿𝐸) ∈ ran 𝐿)
132	131	ad3antrrr 730	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → (𝐷𝐿𝐸) ∈ ran 𝐿)
133		simpl 482	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑤 = 𝑘)
134	133	eleq1d 2813	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
135		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → 𝑣 = 𝑙)
136	135	eleq1d 2813	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ↔ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))))
137	134, 136	anbi12d 632	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ↔ (𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸)))))
138		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑧 = 𝑗)
139		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑤 = 𝑘)
140		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → 𝑣 = 𝑙)
141	139, 140	oveq12d 7405	. . . . . . . . . . 11 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑤𝐼𝑣) = (𝑘𝐼𝑙))
142	138, 141	eleq12d 2822	. . . . . . . . . 10 ⊢ (((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) ∧ 𝑧 = 𝑗) → (𝑧 ∈ (𝑤𝐼𝑣) ↔ 𝑗 ∈ (𝑘𝐼𝑙)))
143	142	cbvrexdva 3218	. . . . . . . . 9 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣) ↔ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙)))
144	137, 143	anbi12d 632	. . . . . . . 8 ⊢ ((𝑤 = 𝑘 ∧ 𝑣 = 𝑙) → (((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣)) ↔ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))))
145	144	cbvopabv 5180	. . . . . . 7 ⊢ {⟨𝑤, 𝑣⟩ ∣ ((𝑤 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑣 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑧 ∈ (𝐷𝐿𝐸)𝑧 ∈ (𝑤𝐼𝑣))} = {⟨𝑘, 𝑙⟩ ∣ ((𝑘 ∈ (𝑃 ∖ (𝐷𝐿𝐸)) ∧ 𝑙 ∈ (𝑃 ∖ (𝐷𝐿𝐸))) ∧ ∃𝑗 ∈ (𝐷𝐿𝐸)𝑗 ∈ (𝑘𝐼𝑙))}
146	8	adantr 480	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐺 ∈ TarskiG)
147	19	adantr 480	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐶 ∈ 𝑃)
148	16	adantr 480	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐵 ∈ 𝑃)
149	12	adantr 480	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐴 ∈ 𝑃)
150	23	adantr 480	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐷 ∈ 𝑃)
151	27	adantr 480	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ∈ 𝑃)
152	28	adantr 480	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ 𝑃)
153	73	ad8antr 740	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝐸 ≠ 𝐷)
154		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐷𝐿𝐸))
155	1, 32, 33, 146, 151, 150, 152, 153, 154	lncom 28549	. . . . . . . . . . . . . 14 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → 𝑓 ∈ (𝐸𝐿𝐷))
156	155	orcd 873	. . . . . . . . . . . . 13 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝑓 ∈ (𝐸𝐿𝐷) ∨ 𝐸 = 𝐷))
157	1, 33, 32, 146, 151, 150, 152, 156	colrot1 28486	. . . . . . . . . . . 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 28455	. . . . . . . . . . . 12 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ⟨“𝐷𝐸𝑓”⟩(cgrG‘𝐺)⟨“𝐴𝐵𝐶”⟩)
160	1, 33, 32, 146, 150, 151, 152, 3, 149, 148, 147, 157, 159	lnxfr 28493	. . . . . . . . . . 11 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
161	1, 33, 32, 146, 149, 147, 148, 160	colrot1 28486	. . . . . . . . . 10 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
162	1, 33, 32, 146, 147, 148, 149, 161	colcom 28485	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
163	34	ad8antr 740	. . . . . . . . 9 ⊢ (((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) ∧ 𝑓 ∈ (𝐷𝐿𝐸)) → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
164	162, 163	pm2.65da 816	. . . . . . . 8 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → ¬ 𝑓 ∈ (𝐷𝐿𝐸))
165	1, 32, 33, 8, 132, 48, 145, 108, 88, 28, 95, 164, 109	hphl 28698	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝑞)
166	70	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → 𝐹 ∈ 𝑃)
167	166	ad2antrr 726	. . . . . . . 8 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → 𝐹 ∈ 𝑃)
168	167	adantr 480	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝐹 ∈ 𝑃)
169		simplrr 777	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) ∧ (𝑓 ∈ 𝑃 ∧ (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))) → 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)
170	1, 32, 33, 8, 132, 28, 145, 95, 165, 168, 169	hpgtr 28695	. . . . . 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 28543	. . . . 5 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (𝑓(𝐾‘𝑦)𝑞 ∧ (𝑦 − 𝑓) = (𝑥 − 𝐶)))
173	171, 172	reximddv 3149	. . . 4 ⊢ (((((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) ∧ 𝑞 ∈ 𝑃) ∧ ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
174	1, 33, 32, 4, 24, 70, 20, 71	ncolrot2 28490	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸))
175		ioran 985	. . . . . . . 8 ⊢ (¬ (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸) ↔ (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
176	174, 175	sylib 218	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐹 ∈ (𝐷𝐿𝐸) ∧ ¬ 𝐷 = 𝐸))
177	176	simpld 494	. . . . . 6 ⊢ (𝜑 → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
178	177	ad4antr 732	. . . . 5 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ¬ 𝐹 ∈ (𝐷𝐿𝐸))
179	1, 2, 32, 33, 6, 36, 131, 145, 87, 166, 178	lnperpex 28730	. . . 4 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑞 ∈ 𝑃 ((𝐷𝐿𝐸)(⟂G‘𝐺)(𝑞𝐿𝑦) ∧ 𝑞((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
180	173, 179	r19.29a 3141	. . 3 ⊢ (((((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) ∧ 𝑦 ∈ 𝑃) ∧ ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
181	1, 33, 32, 5, 10, 14, 42, 3, 21, 25, 2, 79, 30	lnext 28494	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑦 ∈ 𝑃 ⟨“𝐴𝐵𝑥”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑦”⟩)
182	180, 181	r19.29a 3141	. 2 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴𝐿𝐵)) ∧ (𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵)) → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))
183	1, 2, 32, 33, 4, 39, 17, 60	footex 28648	. 2 ⊢ (𝜑 → ∃𝑥 ∈ (𝐴𝐿𝐵)(𝐶𝐿𝑥)(⟂G‘𝐺)(𝐴𝐿𝐵))
184	182, 183	r19.29a 3141	1 ⊢ (𝜑 → ∃𝑓 ∈ 𝑃 (⟨“𝐴𝐵𝐶”⟩(cgrG‘𝐺)⟨“𝐷𝐸𝑓”⟩ ∧ 𝑓((hpG‘𝐺)‘(𝐷𝐿𝐸))𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 ∖ cdif 3911 class class class wbr 5107 {copab 5169 ran crn 5639 ‘cfv 6511 (class class class)co 7387 2c2 12241 ⟨“cs3 14808 Basecbs 17179 distcds 17229 TarskiGcstrkg 28354 Dim_TarskiG≥cstrkgld 28358 Itvcitv 28360 LineGclng 28361 cgrGccgrg 28437 hlGchlg 28527 pInvGcmir 28579 ⟂Gcperpg 28622 hpGchpg 28684

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-oadd 8438 df-er 8671 df-map 8801 df-pm 8802 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-dju 9854 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-fz 13469 df-fzo 13616 df-hash 14296 df-word 14479 df-concat 14536 df-s1 14561 df-s2 14814 df-s3 14815 df-trkgc 28375 df-trkgb 28376 df-trkgcb 28377 df-trkgld 28379 df-trkg 28380 df-cgrg 28438 df-ismt 28460 df-leg 28510 df-hlg 28528 df-mir 28580 df-rag 28621 df-perpg 28623 df-hpg 28685 df-mid 28701 df-lmi 28702

This theorem is referenced by: trgcopyeu 28733 acopy 28760 cgrg3col4 28780

W3C validator