Metamath Proof Explorer

Theorem flatcgra

Description: Flat angles are congruent. (Contributed by Thierry Arnoux, 13-Feb-2023)

Ref Expression
Hypotheses cgracol.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgracol.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
cgracol.m ⊢ − = ( dist ‘ 𝐺 )
cgracol.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
cgracol.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
cgracol.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
cgracol.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
cgracol.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
cgracol.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
cgracol.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
flatcgra.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
flatcgra.2 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
flatcgra.3 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
flatcgra.4 ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
flatcgra.5 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
flatcgra.6 ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
Assertion flatcgra ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 cgracol.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 cgracol.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 cgracol.m ⊢ − = ( dist ‘ 𝐺 )
4 cgracol.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 cgracol.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 cgracol.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 cgracol.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 cgracol.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 cgracol.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 cgracol.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 flatcgra.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
12 flatcgra.2 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
13 flatcgra.3 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
14 flatcgra.4 ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
15 flatcgra.5 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
16 flatcgra.6 ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
17 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
18 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG )
19 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 )
20 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 )
21 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 )
23 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ 𝑃 )
24 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ∈ 𝑃 )
25 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) )
26 1 3 2 18 23 22 20 19 25 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 − 𝐸 ) = ( 𝐴 − 𝐵 ) )
27 26 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 − 𝐵 ) = ( 𝑥 − 𝐸 ) )
28 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) )
29 28 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝑦 ) )
30 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐹 ∈ 𝑃 )
31 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐷 ∈ 𝑃 )
32 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐹 ≠ 𝐸 )
33 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐷 ≠ 𝐸 )
34 1 3 2 4 8 9 10 12 tgbtwncom ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 𝐼 𝐷 ) )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ ( 𝐹 𝐼 𝐷 ) )
36 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) )
37 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) )
38 1 2 18 30 23 31 22 24 32 33 35 36 37 tgbtwnconn22 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ ( 𝑥 𝐼 𝑦 ) )
39 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
40 1 3 2 18 22 23 24 19 20 21 38 39 26 28 tgcgrextend ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 − 𝑦 ) = ( 𝐴 − 𝐶 ) )
41 40 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐴 − 𝐶 ) = ( 𝑥 − 𝑦 ) )
42 1 3 2 18 19 21 22 24 41 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐶 − 𝐴 ) = ( 𝑦 − 𝑥 ) )
43 1 3 17 18 19 20 21 22 23 24 27 29 42 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ )
44 25 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝑥 ) )
45 13 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
46 45 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ≠ 𝐴 )
47 1 3 2 18 20 19 23 22 44 46 tgcgrneq ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ≠ 𝑥 )
48 47 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ≠ 𝐸 )
49 1 2 18 30 23 22 31 32 36 35 tgbtwnconn2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ∈ ( 𝐸 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 𝐼 𝑥 ) ) )
50 48 33 49 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ≠ 𝐸 ∧ 𝐷 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 𝐼 𝑥 ) ) ) )
51 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
52 1 2 51 22 31 23 18 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ↔ ( 𝑥 ≠ 𝐸 ∧ 𝐷 ≠ 𝐸 ∧ ( 𝑥 ∈ ( 𝐸 𝐼 𝐷 ) ∨ 𝐷 ∈ ( 𝐸 𝐼 𝑥 ) ) ) ) )
53 50 52 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 )
54 14 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
55 54 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐵 ≠ 𝐶 )
56 1 3 2 18 20 21 23 24 29 55 tgcgrneq ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ≠ 𝑦 )
57 56 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ≠ 𝐸 )
58 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝐸 ∈ ( 𝐷 𝐼 𝐹 ) )
59 1 2 18 31 23 24 30 33 37 58 tgbtwnconn2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝑦 ) ) )
60 57 32 59 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑦 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝑦 ) ) ) )
61 1 2 51 24 30 23 18 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ↔ ( 𝑦 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ ( 𝑦 ∈ ( 𝐸 𝐼 𝐹 ) ∨ 𝐹 ∈ ( 𝐸 𝐼 𝑦 ) ) ) ) )
62 60 61 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 )
63 43 53 62 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) )
64 1 3 2 4 10 9 6 5 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) )
65 1 3 2 4 8 9 6 7 axtgsegcon ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) )
66 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
67 64 65 66 sylanbrc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝐸 ∈ ( 𝐹 𝐼 𝑥 ) ∧ ( 𝐸 − 𝑥 ) = ( 𝐵 − 𝐴 ) ) ∧ ( 𝐸 ∈ ( 𝐷 𝐼 𝑦 ) ∧ ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐶 ) ) ) )
68 63 67 reximddv2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) )
69 1 2 51 4 5 6 7 8 9 10 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( ( hlG ‘ 𝐺 ) ‘ 𝐸 ) 𝐹 ) ) )
70 68 69 mpbird ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )