Metamath Proof Explorer

Theorem zerocgra

Description: Zero angles are congruent. Zero angles, that is, angles of degree zero, can be expressed by stating that points A and C are on the same ray starting at B , that is, A ( KB ) C . See also flatcgra . (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses zerocgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
zerocgra.a ⊢ ∼ = ( cgrA ‘ 𝐺 )
zerocgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
zerocgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
zerocgra.1 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
zerocgra.2 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
zerocgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
zerocgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
Assertion zerocgra ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 zerocgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 zerocgra.a ⊢ ∼ = ( cgrA ‘ 𝐺 )
3 zerocgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 zerocgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 zerocgra.1 ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
6 zerocgra.2 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
7 zerocgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 zerocgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
9 2 eqcomi ⊢ ( cgrA ‘ 𝐺 ) = ∼
10 9 a1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( cgrA ‘ 𝐺 ) = ∼ )
11 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
12 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐺 ∈ TarskiG )
13 1 11 3 4 7 5 hlgrcl1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
14 13 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐴 ∈ 𝑃 )
15 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐵 ∈ 𝑃 )
16 1 11 3 4 7 5 hlgrcl2 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
17 16 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐶 ∈ 𝑃 )
18 1 11 3 4 8 6 hlgrcl1 ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
19 18 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐷 ∈ 𝑃 )
20 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐸 ∈ 𝑃 )
21 1 11 3 4 8 6 hlgrcl2 ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
22 21 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐹 ∈ 𝑃 )
23 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝑑 ∈ 𝑃 )
24 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝑓 ∈ 𝑃 )
25 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
26 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
27 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) )
28 27 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) )
29 1 25 11 12 15 14 20 23 28 tgcgrcomlr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( 𝐴 ( dist ‘ 𝐺 ) 𝐵 ) = ( 𝑑 ( dist ‘ 𝐺 ) 𝐸 ) )
30 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) )
31 30 eqcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) )
32 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐶 )
33 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 )
34 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 )
35 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐹 )
36 1 11 3 19 22 20 12 35 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐹 ( 𝐾 ‘ 𝐸 ) 𝐷 )
37 1 11 3 24 22 19 12 20 34 36 hltr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐷 )
38 1 11 3 24 19 20 12 37 hlcomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝑓 )
39 1 11 3 23 19 24 12 20 33 38 hltr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → 𝑑 ( 𝐾 ‘ 𝐸 ) 𝑓 )
40 1 25 3 12 15 20 32 39 31 28 tghlsub ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ( 𝐶 ( dist ‘ 𝐺 ) 𝐴 ) = ( 𝑓 ( dist ‘ 𝐺 ) 𝑑 ) )
41 1 25 26 12 14 15 17 23 20 24 29 31 40 trgcgr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑑 𝐸 𝑓 ”⟩ )
42 1 11 3 12 14 15 17 19 20 22 23 24 41 33 34 iscgrad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
43 10 42 breqdi ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
44 43 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ∧ 𝑓 ∈ 𝑃 ) ∧ ( 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
45 1 11 3 18 21 8 4 6 hlne2 ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )
46 1 11 3 13 16 7 4 5 hlne2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
47 46 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
48 1 11 3 8 7 16 4 21 25 45 47 hlcgrex ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
49 48 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) → ∃ 𝑓 ∈ 𝑃 ( 𝑓 ( 𝐾 ‘ 𝐸 ) 𝐹 ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑓 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐶 ) ) )
50 44 49 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ) ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
51 50 anasss ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
52 1 11 3 18 21 8 4 6 hlne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
53 1 11 3 13 16 7 4 5 hlne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
54 53 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
55 1 11 3 8 7 13 4 18 25 52 54 hlcgrex ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝑃 ( 𝑑 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ ( 𝐸 ( dist ‘ 𝐺 ) 𝑑 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝐴 ) ) )
56 51 55 r19.29a ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∼ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )