Theorem trgcopy

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)

	Ref	Expression
Hypotheses	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	trgcopy	⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )

Proof

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