Metamath Proof Explorer

Theorem cgracom

Description: Angle congruence commutes. Theorem 11.7 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 ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion cgracom ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( 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 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
13 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
14 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐺 ∈ TarskiG )
15 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐷 ∈ 𝑃 )
16 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐸 ∈ 𝑃 )
17 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐹 ∈ 𝑃 )
18 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝑥 ∈ 𝑃 )
19 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐵 ∈ 𝑃 )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝑦 ∈ 𝑃 )
21 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) )
22 21 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) )
23 1 12 2 14 16 15 19 18 22 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐷 ( dist ‘ 𝐺 ) 𝐸 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝐵 ) )
24 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) )
25 24 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) )
26 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐴 ∈ 𝑃 )
27 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝐶 ∈ 𝑃 )
28 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
29 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 )
30 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 )
31 1 2 4 14 26 19 27 15 16 17 28 18 12 20 29 30 21 24 cgracgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐷 ( dist ‘ 𝐺 ) 𝐹 ) )
32 31 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐷 ( dist ‘ 𝐺 ) 𝐹 ) = ( 𝑥 ( dist ‘ 𝐺 ) 𝑦 ) )
33 1 12 2 14 15 17 18 20 32 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( 𝐹 ( dist ‘ 𝐺 ) 𝐷 ) = ( 𝑦 ( dist ‘ 𝐺 ) 𝑥 ) )
34 1 12 13 14 15 16 17 18 19 20 23 25 33 trgcgr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ )
35 34 29 30 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ) → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ) )
36 1 2 4 3 5 6 7 8 9 10 11 cgrane1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
37 1 2 4 3 5 6 7 8 9 10 11 cgrane3 ⊢ ( 𝜑 → 𝐸 ≠ 𝐷 )
38 1 2 4 6 9 8 3 5 12 36 37 hlcgrex ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) )
39 1 2 4 3 5 6 7 8 9 10 11 cgrane2 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
40 39 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
41 1 2 4 3 5 6 7 8 9 10 11 cgrane4 ⊢ ( 𝜑 → 𝐸 ≠ 𝐹 )
42 1 2 4 6 9 10 3 7 12 40 41 hlcgrex ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) )
43 reeanv ⊢ ( ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) )
44 38 42 43 sylanbrc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑥 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐷 ) ) ∧ ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ∧ ( 𝐵 ( dist ‘ 𝐺 ) 𝑦 ) = ( 𝐸 ( dist ‘ 𝐺 ) 𝐹 ) ) ) )
45 35 44 reximddv2 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ) )
46 1 2 4 3 8 9 10 5 6 7 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐵 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝐴 ∧ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝐶 ) ) )
47 45 46 mpbird ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )