Metamath Proof Explorer

Theorem cgraswap

Description: Swap rays in a congruence relation. Theorem 11.9 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 5-Mar-2020)

Ref Expression
Hypotheses cgraid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
cgraid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
cgraid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
cgraid.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
cgraid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
cgraid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
cgraid.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
cgraid.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
cgraid.2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
Assertion cgraswap ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )

Proof

Step Hyp Ref Expression
1 cgraid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 cgraid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 cgraid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 cgraid.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
5 cgraid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 cgraid.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 cgraid.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 cgraid.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9 cgraid.2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
10 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
12 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG )
13 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 )
14 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 )
15 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 )
16 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 )
17 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑦 ∈ 𝑃 )
18 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) )
19 1 10 2 12 14 16 14 13 18 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) )
20 19 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝐵 ) )
21 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) )
22 21 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) )
23 eqid ⊢ ( LineG ‘ 𝐺 ) = ( LineG ‘ 𝐺 )
24 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 )
25 1 2 4 16 15 14 12 23 24 hlln ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑥 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) )
26 25 orcd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑥 ∈ ( 𝐶 ( LineG ‘ 𝐺 ) 𝐵 ) ∨ 𝐶 = 𝐵 ) )
27 1 23 2 12 15 14 16 26 colrot1 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐶 ∈ ( 𝐵 ( LineG ‘ 𝐺 ) 𝑥 ) ∨ 𝐵 = 𝑥 ) )
28 eqid ⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
29 1 2 4 16 15 14 12 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ↔ ( 𝑥 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝑥 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝑥 ) ) ) ) )
30 24 29 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑥 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ ( 𝑥 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝑥 ) ) ) )
31 30 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑥 ∈ ( 𝐵 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐵 𝐼 𝑥 ) ) )
32 31 orcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐶 ∈ ( 𝐵 𝐼 𝑥 ) ∨ 𝑥 ∈ ( 𝐵 𝐼 𝐶 ) ) )
33 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 )
34 1 2 4 17 13 14 12 ishlg ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ↔ ( 𝑦 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑦 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝑦 ) ) ) ) )
35 33 34 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑦 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ ( 𝑦 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝑦 ) ) ) )
36 35 simp3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑦 ∈ ( 𝐵 𝐼 𝐴 ) ∨ 𝐴 ∈ ( 𝐵 𝐼 𝑦 ) ) )
37 1 10 2 28 12 14 15 16 14 14 17 13 32 36 22 18 tgcgrsub2 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐴 ) )
38 1 10 11 12 14 15 16 14 17 13 22 37 19 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ⟨“ 𝐵 𝐶 𝑥 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐵 𝑦 𝐴 ”⟩ )
39 1 10 2 12 15 17 axtgcgrrflx ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝐶 ) )
40 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐵 ≠ 𝐶 )
41 1 23 2 12 14 15 16 11 14 17 10 17 13 15 27 38 21 39 40 tgfscgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐴 ( dist ‘ 𝐺 ) 𝐶 ) )
42 1 10 2 12 16 17 13 15 41 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) )
43 42 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
44 1 10 11 12 13 14 15 16 14 17 20 22 43 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ )
45 44 24 33 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ) )
46 9 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
47 8 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
48 1 2 4 6 6 5 3 7 10 46 47 hlcgrex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) )
49 1 2 4 6 6 7 3 5 10 8 9 hlcgrex ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
50 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) )
51 48 49 50 sylanbrc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) )
52 45 51 reximddv2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ) )
53 1 2 4 3 5 6 7 7 6 5 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐴 ) ) )
54 52 53 mpbird ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )