Metamath Proof Explorer


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 ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )