Metamath Proof Explorer

Theorem cgrg3col4

Description: Lemma 11.28 of Schwabhauser p. 102. Extend a congruence of three points with a fourth colinear point. (Contributed by Thierry Arnoux, 8-Oct-2020)

Ref Expression
Hypotheses isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
cgrg3col4.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
cgrg3col4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
cgrg3col4.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgrg3col4.2 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
Assertion cgrg3col4 ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )

Proof

Step Hyp Ref Expression
1 isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3 isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
4 isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
5 isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
6 isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
7 isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
8 isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
9 cgrg3col4.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
10 cgrg3col4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11 cgrg3col4.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12 cgrg3col4.2 ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
13 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
14 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐺 ∈ TarskiG )
15 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐴 ∈ 𝑃 )
16 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐵 ∈ 𝑃 )
17 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝑋 ∈ 𝑃 )
18 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
19 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐷 ∈ 𝑃 )
20 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐸 ∈ 𝑃 )
21 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
22 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
23 1 21 13 18 2 3 4 5 6 7 8 11 cgr3simp1 ⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
25 1 9 13 14 15 16 17 18 19 20 21 22 24 lnext ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ )
26 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
27 14 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
28 17 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
29 15 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
30 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
31 19 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
32 16 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
33 20 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
34 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ )
35 1 21 13 18 27 29 32 28 31 33 30 34 cgr3simp3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) )
36 1 21 13 27 28 29 30 31 35 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) )
37 1 21 13 18 27 29 32 28 31 33 30 34 cgr3simp2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) )
38 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
39 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐹 ∈ 𝑃 )
40 simpr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 = 𝐶 )
41 40 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐴 = 𝐶 )
42 41 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) )
43 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐺 ∈ TarskiG )
44 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐴 ∈ 𝑃 )
45 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐶 ∈ 𝑃 )
46 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 ∈ 𝑃 )
47 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐹 ∈ 𝑃 )
48 1 21 13 18 2 3 4 5 6 7 8 11 cgr3simp3 ⊢ ( 𝜑 → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐷 ) )
49 1 21 13 2 5 3 8 6 48 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐴 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐹 ) )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐹 ) )
51 1 21 13 43 44 45 46 47 50 40 tgcgreq ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → 𝐷 = 𝐹 )
52 51 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → 𝐷 = 𝐹 )
53 52 oveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
54 35 42 53 3eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
55 1 21 13 27 28 38 30 39 54 tgcgrcomlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) )
56 36 37 55 3jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) )
57 1 21 13 18 27 29 32 38 28 31 33 39 30 tgcgr4 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) ) ) )
58 26 56 57 mpbir2and ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
59 58 ex ⊢ ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
60 59 reximdva ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑦 ”⟩ → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
61 25 60 mpd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
62 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
63 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐺 ∈ TarskiG )
64 63 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐺 ∈ TarskiG )
65 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐵 ∈ 𝑃 )
66 65 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐵 ∈ 𝑃 )
67 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐴 ∈ 𝑃 )
68 67 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐴 ∈ 𝑃 )
69 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝑋 ∈ 𝑃 )
70 69 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑋 ∈ 𝑃 )
71 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐸 ∈ 𝑃 )
72 71 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐸 ∈ 𝑃 )
73 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐷 ∈ 𝑃 )
74 73 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐷 ∈ 𝑃 )
75 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝑥 ∈ 𝑃 )
76 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
77 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) )
78 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
79 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
80 1 13 9 63 65 67 69 79 ncolne1 ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐵 ≠ 𝐴 )
81 80 necomd ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐴 ≠ 𝐵 )
82 1 21 13 63 67 65 73 71 78 81 tgcgrneq ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐷 ≠ 𝐸 )
83 82 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → 𝐷 ≠ 𝐸 )
84 83 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ 𝐷 = 𝐸 )
85 ioran ⊢ ( ¬ ( 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) ↔ ( ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∧ ¬ 𝐷 = 𝐸 ) )
86 77 84 85 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ∨ 𝐷 = 𝐸 ) )
87 1 9 13 64 74 72 75 86 ncolcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝑥 ∈ ( 𝐸 𝐿 𝐷 ) ∨ 𝐸 = 𝐷 ) )
88 1 9 13 64 72 74 75 87 ncolrot1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ¬ ( 𝐸 ∈ ( 𝐷 𝐿 𝑥 ) ∨ 𝐷 = 𝑥 ) )
89 1 21 13 2 3 4 6 7 23 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) )
90 89 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) )
91 1 21 13 9 62 64 66 68 70 72 74 75 76 88 90 trgcopy ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ∧ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑥 ) )
92 11 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
93 64 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
94 66 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
95 68 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
96 70 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
97 72 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
98 74 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
99 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
100 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ )
101 1 21 13 18 93 94 95 96 97 98 99 100 cgr3simp2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) )
102 1 21 13 18 93 94 95 96 97 98 99 100 cgr3simp3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐸 ) )
103 1 21 13 93 96 94 99 97 102 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) )
104 45 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
105 47 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐹 ∈ 𝑃 )
106 1 21 13 93 95 96 98 99 101 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) )
107 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐴 = 𝐶 )
108 107 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) )
109 51 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → 𝐷 = 𝐹 )
110 109 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
111 106 108 110 3eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐹 ) )
112 1 21 13 93 96 104 99 105 111 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) )
113 101 103 112 3jca ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) )
114 1 21 13 18 93 95 94 104 96 98 97 105 99 tgcgr4 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) ) ) )
115 92 113 114 mpbir2and ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
116 115 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
117 116 adantrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ∧ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑥 ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
118 117 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ( ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐵 𝐴 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐸 𝐷 𝑦 ”⟩ ∧ 𝑦 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐸 𝐿 𝐷 ) ) 𝑥 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
119 91 118 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
120 1 9 13 63 67 69 65 79 ncoltgdim2 ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → 𝐺 DimTarskiG≥ 2 )
121 1 13 9 63 120 73 71 82 tglowdim2ln ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑥 ∈ 𝑃 ¬ 𝑥 ∈ ( 𝐷 𝐿 𝐸 ) )
122 119 121 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝐴 = 𝐶 ) ∧ ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
123 61 122 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐴 = 𝐶 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
124 1 9 13 2 3 5 10 12 colcom ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
125 1 9 13 2 5 3 10 124 colrot1 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
126 1 9 13 2 3 5 10 18 6 8 21 125 49 lnext ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ )
127 126 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ )
128 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
129 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐺 ∈ TarskiG )
130 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝑋 ∈ 𝑃 )
131 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐴 ∈ 𝑃 )
132 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝑦 ∈ 𝑃 )
133 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐷 ∈ 𝑃 )
134 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐶 ∈ 𝑃 )
135 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐹 ∈ 𝑃 )
136 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ )
137 1 21 13 18 129 131 134 130 133 135 132 136 cgr3simp3 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐷 ) )
138 1 21 13 129 130 131 132 133 137 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) )
139 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐵 ∈ 𝑃 )
140 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐸 ∈ 𝑃 )
141 125 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐶 ∈ ( 𝐴 𝐿 𝑋 ) ∨ 𝐴 = 𝑋 ) )
142 23 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) )
143 1 21 13 18 2 3 4 5 6 7 8 11 cgr3simp2 ⊢ ( 𝜑 → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) )
144 1 21 13 2 4 5 7 8 143 tgcgrcomlr ⊢ ( 𝜑 → ( 𝐶 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐸 ) )
145 144 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝐸 ) )
146 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → 𝐴 ≠ 𝐶 )
147 1 9 13 129 131 134 130 18 133 135 21 139 132 140 141 136 142 145 146 tgfscgr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝑋 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐸 ) )
148 1 21 13 129 130 139 132 140 147 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) )
149 1 21 13 18 129 131 134 130 133 135 132 136 cgr3simp2 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) )
150 138 148 149 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) )
151 1 21 13 18 129 131 139 134 130 133 140 135 132 tgcgr4 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ( ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ( ( 𝐴 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑦 ) ∧ ( 𝐶 ( dist ‘ 𝐺 ) 𝑋 ) = ( 𝐹 ( dist ‘ 𝐺 ) 𝑦 ) ) ) ) )
152 128 150 151 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
153 152 ex ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝑦 ∈ 𝑃 ) → ( ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ → ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
154 153 reximdva ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ( ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐹 𝑦 ”⟩ → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ ) )
155 127 154 mpd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )
156 123 155 pm2.61dane ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ⟨“ 𝐴 𝐵 𝐶 𝑋 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 𝑦 ”⟩ )