Metamath Proof Explorer

Theorem acopy

Description: Angle construction. Theorem 11.15 of Schwabhauser p. 98. This is Hilbert's axiom III.4 for geometry. (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 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
Assertion acopy ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )

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 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
15 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐺 ∈ TarskiG )
16 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐴 ∈ 𝑃 )
17 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐵 ∈ 𝑃 )
18 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐶 ∈ 𝑃 )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ∈ 𝑃 )
20 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐸 ∈ 𝑃 )
21 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐹 ∈ 𝑃 )
22 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
23 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝐷 ∈ 𝑃 )
24 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
25 simprl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
26 1 2 14 19 23 20 15 11 25 hlln ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ∈ ( 𝐷 𝐿 𝐸 ) )
27 1 2 14 19 23 20 15 25 hlne1 ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → 𝑑 ≠ 𝐸 )
28 1 2 11 15 23 20 21 19 24 26 27 ncolncol ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ¬ ( 𝑑 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
29 simprr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) )
30 29 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝑑 ) )
31 1 3 2 15 17 16 20 19 30 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝑑 − 𝐸 ) )
32 1 3 2 11 14 15 16 17 18 19 20 21 22 28 31 trgcopy ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) )
33 15 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐺 ∈ TarskiG )
34 16 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐴 ∈ 𝑃 )
35 17 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐵 ∈ 𝑃 )
36 18 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐶 ∈ 𝑃 )
37 19 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝑑 ∈ 𝑃 )
38 20 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐸 ∈ 𝑃 )
39 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝑓 ∈ 𝑃 )
40 1 2 11 4 5 6 7 12 ncolne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
41 40 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐴 ≠ 𝐵 )
42 1 11 2 4 6 7 5 12 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
43 1 2 11 4 6 7 5 42 ncolne1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
44 43 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐵 ≠ 𝐶 )
45 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ )
46 1 2 33 14 34 35 36 37 38 39 41 44 45 cgrcgra ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ )
47 23 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐷 ∈ 𝑃 )
48 25 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
49 1 2 14 37 47 38 33 48 hlcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → 𝐷 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑑 )
50 1 2 14 33 34 35 36 37 38 39 46 47 49 cgrahl1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ )
51 50 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ) )
52 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 )
53 15 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝐺 ∈ TarskiG )
54 19 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝑑 ∈ 𝑃 )
55 20 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝐸 ∈ 𝑃 )
56 27 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝑑 ≠ 𝐸 )
57 1 2 11 4 8 9 10 13 ncolne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
58 1 2 11 4 8 9 57 tgelrnln ⊢ ( 𝜑 → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
59 58 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → ( 𝐷 𝐿 𝐸 ) ∈ ran 𝐿 )
60 26 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝑑 ∈ ( 𝐷 𝐿 𝐸 ) )
61 1 2 11 4 8 9 57 tglinerflx2 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐿 𝐸 ) )
62 61 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝐸 ∈ ( 𝐷 𝐿 𝐸 ) )
63 1 2 11 53 54 55 56 56 59 60 62 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → ( 𝐷 𝐿 𝐸 ) = ( 𝑑 𝐿 𝐸 ) )
64 63 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) )
65 64 breqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → ( 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ↔ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) )
66 52 65 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
67 66 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) → ( 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )
68 51 67 anim12d ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) ∧ 𝑓 ∈ 𝑃 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) )
69 68 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ( ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑑 𝐿 𝐸 ) ) 𝐹 ) → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) )
70 32 69 mpd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) ) → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )
71 40 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
72 1 2 14 9 6 5 4 8 3 57 71 hlcgrex ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ( 𝑑 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 − 𝑑 ) = ( 𝐵 − 𝐴 ) ) )
73 70 72 r19.29a ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )