Metamath Proof Explorer

Theorem acopyeu

Description: Angle construction. Theorem 11.15 of Schwabhauser p. 98. This is Hilbert's axiom III.4 for geometry. Akin to a uniqueness theorem, this states that if two points X and Y both fulfill the conditions, then they are on the same half-line. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses dfcgra2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
dfcgra2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
dfcgra2.m ⊢ − = ( dist ‘ 𝐺 )
dfcgra2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
dfcgra2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
dfcgra2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
dfcgra2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
dfcgra2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
dfcgra2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
dfcgra2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
acopy.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
acopy.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
acopy.2 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
acopyeu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
acopyeu.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
acopyeu.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
acopyeu.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
acopyeu.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑌 ”⟩ )
acopyeu.3 ⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
acopyeu.4 ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
Assertion acopyeu ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝑌 )

Proof

Step Hyp Ref Expression
1 dfcgra2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 dfcgra2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 dfcgra2.m ⊢ − = ( dist ‘ 𝐺 )
4 dfcgra2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 dfcgra2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 dfcgra2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 dfcgra2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 dfcgra2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 dfcgra2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 dfcgra2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 acopy.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
12 acopy.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
13 acopy.2 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
14 acopyeu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
15 acopyeu.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
16 acopyeu.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
17 acopyeu.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
18 acopyeu.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑌 ”⟩ )
19 acopyeu.3 ⊢ ( 𝜑 → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
20 acopyeu.4 ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
21 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑋 ∈ 𝑃 )
22 21 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑋 ∈ 𝑃 )
23 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ∈ 𝑃 )
24 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑌 ∈ 𝑃 )
25 24 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑌 ∈ 𝑃 )
26 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐺 ∈ TarskiG )
27 26 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐺 ∈ TarskiG )
28 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐸 ∈ 𝑃 )
29 28 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐸 ∈ 𝑃 )
30 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐴 ∈ 𝑃 )
31 30 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐴 ∈ 𝑃 )
32 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐵 ∈ 𝑃 )
33 32 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐵 ∈ 𝑃 )
34 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐶 ∈ 𝑃 )
35 34 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐶 ∈ 𝑃 )
36 simplr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ∈ 𝑃 )
37 36 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑑 ∈ 𝑃 )
38 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐹 ∈ 𝑃 )
39 38 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐹 ∈ 𝑃 )
40 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
41 40 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
42 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐷 ∈ 𝑃 )
43 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
44 simprl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 )
45 1 2 16 36 42 28 26 11 44 hlln ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ∈ ( 𝐷 𝐿 𝐸 ) )
46 1 2 16 36 42 28 26 44 hlne1 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ≠ 𝐸 )
47 1 2 11 26 42 28 38 36 43 45 46 ncolncol ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ¬ ( 𝑑 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
48 47 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑑 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
49 simprr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) )
50 1 3 2 26 28 36 32 30 49 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝑑 − 𝐸 ) = ( 𝐴 − 𝐵 ) )
51 50 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝑑 − 𝐸 ) )
52 51 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝑑 − 𝐸 ) )
53 simpl ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → 𝑢 = 𝑎 )
54 53 eleq1d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑢 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ↔ 𝑎 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) )
55 simpr ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → 𝑣 = 𝑏 )
56 55 eleq1d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑣 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ↔ 𝑏 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) )
57 54 56 anbi12d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) ) )
58 simpr ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑤 = 𝑡 )
59 simpll ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑢 = 𝑎 )
60 simplr ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑣 = 𝑏 )
61 59 60 oveq12d ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → ( 𝑢 𝐼 𝑣 ) = ( 𝑎 𝐼 𝑏 ) )
62 58 61 eleq12d ⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → ( 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
63 62 cbvrexdva ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ∃ 𝑤 ∈ ( 𝑑 𝐿 𝐸 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ↔ ∃ 𝑡 ∈ ( 𝑑 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
64 57 63 anbi12d ⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝑑 𝐿 𝐸 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑑 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
65 64 cbvopabv ⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝑑 𝐿 𝐸 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑑 𝐿 𝐸 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑑 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
66 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 ∈ 𝑃 )
67 simprll ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ )
68 simprrl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ )
69 1 2 11 26 36 28 46 tgelrnln ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝑑 𝐿 𝐸 ) ∈ ran 𝐿 )
70 69 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ( 𝑑 𝐿 𝐸 ) ∈ ran 𝐿 )
71 1 2 11 26 36 28 46 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐸 ∈ ( 𝑑 𝐿 𝐸 ) )
72 71 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐸 ∈ ( 𝑑 𝐿 𝐸 ) )
73 42 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝐷 ∈ 𝑃 )
74 1 11 2 4 6 7 5 12 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
75 1 2 3 4 5 6 7 8 9 14 17 11 74 cgrancol ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
76 1 11 2 4 8 9 14 75 ncolcom ⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
77 76 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑋 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
78 simprlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 )
79 1 2 16 66 22 29 27 11 78 hlln ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 ∈ ( 𝑋 𝐿 𝐸 ) )
80 1 2 16 66 22 29 27 78 hlne1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 ≠ 𝐸 )
81 1 2 11 27 22 29 73 66 77 79 80 ncolncol ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑥 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
82 1 11 2 27 29 73 66 81 ncolcom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
83 pm2.45 ⊢ ( ¬ ( 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) → ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) )
84 82 83 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) )
85 1 2 11 4 8 9 10 13 ncolne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
86 1 2 11 4 8 9 85 tgelrnln ⊢ ( 𝜑 → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
87 86 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
88 1 2 11 4 8 9 85 tglinerflx2 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐿 𝐸 ) )
89 88 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐸 ∈ ( 𝐷 𝐿 𝐸 ) )
90 1 2 11 26 36 28 46 46 87 45 89 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐷 𝐿 𝐸 ) = ( 𝑑 𝐿 𝐸 ) )
91 90 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ( 𝐷 𝐿 𝐸 ) = ( 𝑑 𝐿 𝐸 ) )
92 84 91 neleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ 𝑥 ∈ ( 𝑑 𝐿 𝐸 ) )
93 1 2 11 27 70 29 65 16 72 66 22 92 78 hphl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝑋 )
94 90 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) )
95 94 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) )
96 19 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
97 95 96 breqdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 )
98 1 2 11 27 70 66 65 22 93 39 97 hpgtr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 )
99 1 2 3 4 5 6 7 8 9 15 18 11 74 cgrancol ⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
100 1 11 2 4 8 9 15 99 ncolcom ⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
101 100 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑌 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
102 simprrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 )
103 1 2 16 23 25 29 27 11 102 hlln ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ∈ ( 𝑌 𝐿 𝐸 ) )
104 1 2 16 23 25 29 27 102 hlne1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ≠ 𝐸 )
105 1 2 11 27 25 29 73 23 101 103 104 ncolncol ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑦 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
106 1 11 2 27 29 73 23 105 ncolcom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ ( 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
107 pm2.45 ⊢ ( ¬ ( 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) → ¬ 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) )
108 106 107 syl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ 𝑦 ∈ ( 𝐷 𝐿 𝐸 ) )
109 108 91 neleqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → ¬ 𝑦 ∈ ( 𝑑 𝐿 𝐸 ) )
110 1 2 11 27 70 29 65 16 72 23 25 109 102 hphl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝑌 )
111 20 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
112 95 111 breqdi ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 )
113 1 2 11 27 70 23 65 25 110 39 112 hpgtr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 )
114 1 3 2 11 16 27 31 33 35 37 29 39 41 48 52 65 66 23 67 68 98 113 trgcopyeulem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑥 = 𝑦 )
115 114 78 eqbrtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑋 )
116 1 2 16 23 22 29 27 115 hlcomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝑦 )
117 1 2 16 22 23 25 27 29 116 102 hltr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ) → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝑌 )
118 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
119 1 2 16 26 30 32 34 42 28 21 118 36 44 cgrahl1 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑋 ”⟩ )
120 1 2 11 4 5 6 7 12 ncolne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
121 120 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐴 ≠ 𝐵 )
122 1 2 16 26 30 32 34 36 28 21 3 121 51 iscgra1 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑋 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ) )
123 119 122 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) )
124 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑌 ”⟩ )
125 1 2 16 26 30 32 34 42 28 24 124 36 44 cgrahl1 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑌 ”⟩ )
126 1 2 16 26 30 32 34 36 28 24 3 121 51 iscgra1 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑌 ”⟩ ↔ ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) )
127 125 126 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) )
128 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) )
129 123 127 128 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝑋 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑦 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝑌 ) ) )
130 117 129 r19.29vva ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝑌 )
131 120 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
132 1 2 16 9 6 5 4 8 3 85 131 hlcgrex ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) )
133 130 132 r19.29a ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝑌 )