Metamath Proof Explorer

Theorem cgratr

Description: Angle congruence is transitive. Theorem 11.8 of Schwabhauser p. 97. (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 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
cgracom.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
cgracom.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
cgracom.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
cgracom.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
cgratr.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
cgratr.i ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
cgratr.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
cgratr.1 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
Assertion cgratr ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( 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 cgracom.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 cgracom.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 cgracom.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 cgracom.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12 cgratr.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
13 cgratr.i ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
14 cgratr.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
15 cgratr.1 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
16 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
17 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
18 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐺 ∈ TarskiG )
19 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐴 ∈ 𝑃 )
20 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐵 ∈ 𝑃 )
21 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝐶 ∈ 𝑃 )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑥 ∈ 𝑃 )
23 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑈 ∈ 𝑃 )
24 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑦 ∈ 𝑃 )
25 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) )
26 25 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) )
27 1 16 2 18 20 19 23 22 26 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑈 ) )
28 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) )
29 28 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) )
30 18 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
31 19 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐴 ∈ 𝑃 )
32 20 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ∈ 𝑃 )
33 21 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐶 ∈ 𝑃 )
34 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑢 ∈ 𝑃 )
35 9 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ 𝑃 )
36 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑣 ∈ 𝑃 )
37 simpr1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ )
38 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑣 ( dist ‘ 𝐺 ) 𝑢 ) )
39 22 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ∈ 𝑃 )
40 24 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ∈ 𝑃 )
41 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ∈ 𝑃 )
42 10 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐹 ∈ 𝑃 )
43 23 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑈 ∈ 𝑃 )
44 14 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐽 ∈ 𝑃 )
45 12 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐻 ∈ 𝑃 )
46 15 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
47 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 )
48 47 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 )
49 1 2 4 30 41 35 42 45 43 44 46 39 48 cgrahl1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝑈 𝐽 ”⟩ )
50 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 )
51 50 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 )
52 1 2 4 30 41 35 42 39 43 44 49 40 51 cgrahl2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑥 𝑈 𝑦 ”⟩ )
53 simpr2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 )
54 simpr3 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 )
55 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑢 ( dist ‘ 𝐺 ) 𝐸 ) )
56 55 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑢 ( dist ‘ 𝐺 ) 𝐸 ) = ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) )
57 1 16 2 30 34 35 31 32 56 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) )
58 26 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) )
59 57 58 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) )
60 1 16 2 17 30 31 32 33 34 35 36 37 cgr3simp2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑣 ) )
61 29 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) )
62 60 61 eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) )
63 1 2 4 30 41 35 42 39 43 40 52 34 16 36 53 54 59 62 cgracgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑢 ( dist ‘ 𝐺 ) 𝑣 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) )
64 1 16 2 30 34 36 39 40 63 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑣 ( dist ‘ 𝐺 ) 𝑢 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
65 38 64 eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) ∧ 𝑢 ∈ 𝑃 ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
66 1 2 4 3 5 6 7 8 9 10 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
67 11 66 mpbid ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
68 67 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ∃ 𝑢 ∈ 𝑃 ∃ 𝑣 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑢 𝐸 𝑣 ”⟩ ∧ 𝑢 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑣 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
69 65 68 r19.29vva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
70 1 16 17 18 19 20 21 22 23 24 27 29 69 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑈 𝑦 ”⟩ )
71 70 47 50 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑈 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ) )
72 1 2 4 3 8 9 10 12 13 14 15 cgrane3 ⊢ ( 𝜑 → 𝑈 ≠ 𝐻 )
73 72 necomd ⊢ ( 𝜑 → 𝐻 ≠ 𝑈 )
74 1 2 4 3 5 6 7 8 9 10 11 cgrane1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
75 74 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
76 1 2 4 13 6 5 3 12 16 73 75 hlcgrex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) )
77 1 2 4 3 8 9 10 12 13 14 15 cgrane4 ⊢ ( 𝜑 → 𝑈 ≠ 𝐽 )
78 77 necomd ⊢ ( 𝜑 → 𝐽 ≠ 𝑈 )
79 1 2 4 3 5 6 7 8 9 10 11 cgrane2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
80 1 2 4 13 6 7 3 14 16 78 79 hlcgrex ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
81 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) )
82 76 80 81 sylanbrc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ∧ ( 𝑈 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) )
83 71 82 reximddv2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑈 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ) )
84 1 2 4 3 5 6 7 12 13 14 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝑈 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝑈 ) 𝐻 ∧ 𝑦 ( 𝐾 ‘ 𝑈 ) 𝐽 ) ) )
85 83 84 mpbird ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )