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