Metamath Proof Explorer

Theorem tgasa1

Description: Second congruence theorem: ASA. (Angle-Side-Angle): If two pairs of angles of two triangles are equal in measurement, and the included sides are equal in length, then the triangles are congruent. Theorem 11.50 of Schwabhauser p. 108. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Hypotheses tgsas.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgsas.m ⊢ − = ( dist ‘ 𝐺 )
tgsas.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgsas.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgsas.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgsas.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgsas.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgsas.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgsas.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgsas.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
tgasa.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgasa.1 ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
tgasa.2 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
tgasa.3 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
tgasa.4 ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )
Assertion tgasa1 ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tgsas.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgsas.m ⊢ − = ( dist ‘ 𝐺 )
3 tgsas.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgsas.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tgsas.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 tgsas.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 tgsas.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 tgsas.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 tgsas.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 tgsas.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 tgasa.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
12 tgasa.1 ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
13 tgasa.2 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
14 tgasa.3 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
15 tgasa.4 ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )
16 simprr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) )
17 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
18 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ∈ 𝑃 )
19 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ∈ 𝑃 )
20 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐸 ∈ 𝑃 )
21 1 3 2 4 5 6 7 8 9 10 14 11 12 cgrancol ⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
23 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
24 simplr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ∈ 𝑃 )
25 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
26 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐴 ∈ 𝑃 )
27 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐵 ∈ 𝑃 )
28 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
29 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐺 ∈ TarskiG )
30 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐷 ∈ 𝑃 )
31 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐸 ∈ 𝑃 )
32 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐹 ∈ 𝑃 )
33 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐴 ∈ 𝑃 )
34 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐵 ∈ 𝑃 )
35 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → 𝐶 ∈ 𝑃 )
36 1 3 4 23 5 6 7 8 9 10 14 cgracom ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
37 36 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
38 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) )
39 1 11 3 29 30 32 31 38 colcom ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → ( 𝐸 ∈ ( 𝐹 𝐿 𝐷 ) ∨ 𝐹 = 𝐷 ) )
40 1 11 3 29 32 30 31 39 colrot1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → ( 𝐹 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
41 1 3 2 29 30 31 32 33 34 35 37 11 40 cgracol ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
42 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
43 41 42 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ¬ ( 𝐸 ∈ ( 𝐷 𝐿 𝐹 ) ∨ 𝐷 = 𝐹 ) )
44 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
45 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
46 simprl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
47 1 3 23 17 26 27 25 19 20 18 45 24 46 cgrahl2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ )
48 1 3 23 4 5 6 7 8 9 10 14 cgrane1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
49 1 3 23 5 5 6 4 48 hlid ⊢ ( 𝜑 → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
51 1 3 23 4 5 6 7 8 9 10 14 cgrane2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
52 51 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
53 1 3 23 7 5 6 4 52 hlid ⊢ ( 𝜑 → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
55 1 2 3 4 5 6 8 9 13 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
57 16 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑓 ) )
58 1 3 23 17 26 27 25 19 20 24 47 26 2 25 50 54 56 57 cgracgr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝑓 ) )
59 1 2 3 17 26 25 19 24 58 tgcgrcomlr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝑓 − 𝐷 ) )
60 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
61 1 2 44 17 25 26 27 24 19 20 59 60 57 trgcgr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑓 𝐷 𝐸 ”⟩ )
62 1 3 11 4 7 5 6 12 ncolne1 ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐶 ≠ 𝐴 )
64 1 2 3 17 25 26 24 19 59 63 tgcgrneq ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ≠ 𝐷 )
65 1 3 23 24 18 19 17 64 hlid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐷 ) 𝑓 )
66 1 3 23 4 7 5 6 10 8 9 15 cgrane4 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
67 66 necomd ⊢ ( 𝜑 → 𝐸 ≠ 𝐷 )
68 1 3 23 9 5 8 4 67 hlid ⊢ ( 𝜑 → 𝐸 ( ( hlG ‘ 𝐺 ) ‘ 𝐷 ) 𝐸 )
69 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐸 ( ( hlG ‘ 𝐺 ) ‘ 𝐷 ) 𝐸 )
70 1 3 23 17 25 26 27 24 19 20 24 20 61 65 69 iscgrad ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑓 𝐷 𝐸 ”⟩ )
71 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐷 ≠ 𝐸 )
72 1 3 17 23 24 19 20 64 71 cgraswap ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝑓 𝐷 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑓 ”⟩ )
73 1 3 17 23 25 26 27 24 19 20 70 20 19 24 72 cgratr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑓 ”⟩ )
74 1 3 23 4 7 5 6 10 8 9 15 cgrane3 ⊢ ( 𝜑 → 𝐷 ≠ 𝐹 )
75 74 necomd ⊢ ( 𝜑 → 𝐹 ≠ 𝐷 )
76 1 3 4 23 10 8 9 75 66 cgraswap ⊢ ( 𝜑 → ⟨“ 𝐹 𝐷 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝐹 ”⟩ )
77 1 3 4 23 7 5 6 10 8 9 15 9 8 10 76 cgratr ⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝐹 ”⟩ )
78 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝐹 ”⟩ )
79 1 3 11 4 9 8 67 tgelrnln ⊢ ( 𝜑 → ( 𝐸 𝐿 𝐷 ) ∈ ran 𝐿 )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐸 𝐿 𝐷 ) ∈ ran 𝐿 )
81 simpl ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → 𝑎 = 𝑢 )
82 81 eleq1d ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ↔ 𝑢 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) )
83 simpr ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → 𝑏 = 𝑣 )
84 83 eleq1d ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( 𝑏 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ↔ 𝑣 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) )
85 82 84 anbi12d ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) ↔ ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) ) )
86 simpr ⊢ ( ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) ∧ 𝑡 = 𝑤 ) → 𝑡 = 𝑤 )
87 simpll ⊢ ( ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) ∧ 𝑡 = 𝑤 ) → 𝑎 = 𝑢 )
88 simplr ⊢ ( ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) ∧ 𝑡 = 𝑤 ) → 𝑏 = 𝑣 )
89 87 88 oveq12d ⊢ ( ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) ∧ 𝑡 = 𝑤 ) → ( 𝑎 𝐼 𝑏 ) = ( 𝑢 𝐼 𝑣 ) )
90 86 89 eleq12d ⊢ ( ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) ∧ 𝑡 = 𝑤 ) → ( 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) )
91 90 cbvrexdva ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ∃ 𝑡 ∈ ( 𝐸 𝐿 𝐷 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑤 ∈ ( 𝐸 𝐿 𝐷 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) )
92 85 91 anbi12d ⊢ ( ( 𝑎 = 𝑢 ∧ 𝑏 = 𝑣 ) → ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐸 𝐿 𝐷 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝐸 𝐿 𝐷 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) ) )
93 92 cbvopabv ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐸 𝐿 𝐷 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐸 𝐿 𝐷 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝐸 𝐿 𝐷 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) }
94 1 3 11 4 9 8 67 tglinerflx1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐸 𝐿 𝐷 ) )
95 94 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐸 ∈ ( 𝐸 𝐿 𝐷 ) )
96 1 11 3 4 8 9 10 21 ncolcom ⊢ ( 𝜑 → ¬ ( 𝐹 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
97 pm2.45 ⊢ ( ¬ ( 𝐹 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) → ¬ 𝐹 ∈ ( 𝐸 𝐿 𝐷 ) )
98 96 97 syl ⊢ ( 𝜑 → ¬ 𝐹 ∈ ( 𝐸 𝐿 𝐷 ) )
99 98 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ¬ 𝐹 ∈ ( 𝐸 𝐿 𝐷 ) )
100 1 3 23 24 18 20 17 46 hlcomd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝑓 )
101 1 3 11 17 80 20 93 23 95 18 24 99 100 hphl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑓 )
102 1 3 11 17 80 18 93 24 101 hpgcom ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝐹 )
103 1 3 11 4 79 10 93 98 hpgid ⊢ ( 𝜑 → 𝐹 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝐹 )
104 103 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝐹 )
105 1 3 2 17 25 26 27 20 19 18 11 28 43 24 18 23 73 78 102 104 acopyeu ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐷 ) 𝐹 )
106 1 3 23 24 18 19 17 11 105 hlln ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ∈ ( 𝐹 𝐿 𝐷 ) )
107 1 3 11 4 10 8 75 tglinerflx1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐹 𝐿 𝐷 ) )
108 107 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ∈ ( 𝐹 𝐿 𝐷 ) )
109 1 3 23 4 5 6 7 8 9 10 14 cgrane4 ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
110 109 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐸 ≠ 𝐹 )
111 1 3 23 24 18 20 17 11 46 hlln ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ∈ ( 𝐹 𝐿 𝐸 ) )
112 1 3 11 17 20 18 24 110 111 lncom ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 ∈ ( 𝐸 𝐿 𝐹 ) )
113 1 3 11 17 20 18 110 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝐹 ∈ ( 𝐸 𝐿 𝐹 ) )
114 1 3 11 17 18 19 20 18 22 106 108 112 113 tglineinteq ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → 𝑓 = 𝐹 )
115 114 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐸 − 𝑓 ) = ( 𝐸 − 𝐹 ) )
116 16 115 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
117 109 necomd ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
118 1 3 23 9 6 7 4 10 2 117 51 hlcgrex ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( 𝑓 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 − 𝑓 ) = ( 𝐵 − 𝐶 ) ) )
119 116 118 r19.29a ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )