Metamath Proof Explorer


Theorem ercgrg

Description: The shape congruence relation is an equivalence relation. Statement 4.4 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019)

Ref Expression
Hypothesis ercgrg.p 𝑃 = ( Base ‘ 𝐺 )
Assertion ercgrg ( 𝐺 ∈ TarskiG → ( cgrG ‘ 𝐺 ) Er ( 𝑃pm ℝ ) )

Proof

Step Hyp Ref Expression
1 ercgrg.p 𝑃 = ( Base ‘ 𝐺 )
2 df-cgrg cgrG = ( 𝑔 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎 ( ( 𝑎𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎𝑗 ) ) = ( ( 𝑏𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏𝑗 ) ) ) ) } )
3 2 relmptopab Rel ( cgrG ‘ 𝐺 )
4 3 a1i ( 𝐺 ∈ TarskiG → Rel ( cgrG ‘ 𝐺 ) )
5 eqid ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
6 eqid ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
7 1 5 6 iscgrg ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ↔ ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑦 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) ) ) ) )
8 7 biimpa ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑦 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) ) ) )
9 8 simpld ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑦 ∈ ( 𝑃pm ℝ ) ) )
10 9 ancomd ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) )
11 8 simprd ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) ) )
12 11 simpld ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → dom 𝑥 = dom 𝑦 )
13 12 eqcomd ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → dom 𝑦 = dom 𝑥 )
14 simpl ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) )
15 simprl ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → 𝑖 ∈ dom 𝑦 )
16 12 adantr ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → dom 𝑥 = dom 𝑦 )
17 15 16 eleqtrrd ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → 𝑖 ∈ dom 𝑥 )
18 simprr ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → 𝑗 ∈ dom 𝑦 )
19 18 16 eleqtrrd ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → 𝑗 ∈ dom 𝑥 )
20 11 simprd ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
21 20 r19.21bi ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ 𝑖 ∈ dom 𝑥 ) → ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
22 21 r19.21bi ( ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ 𝑖 ∈ dom 𝑥 ) ∧ 𝑗 ∈ dom 𝑥 ) → ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
23 14 17 19 22 syl21anc ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
24 23 eqcomd ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ) ) → ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) )
25 24 ralrimivva ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) )
26 13 25 jca ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( dom 𝑦 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) ) )
27 1 5 6 iscgrg ( 𝐺 ∈ TarskiG → ( 𝑦 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) ) ) ) )
28 27 adantr ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( 𝑦 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) ) ) ) )
29 10 26 28 mpbir2and ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → 𝑦 ( cgrG ‘ 𝐺 ) 𝑥 )
30 9 simpld ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → 𝑥 ∈ ( 𝑃pm ℝ ) )
31 30 adantrr ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → 𝑥 ∈ ( 𝑃pm ℝ ) )
32 1 5 6 iscgrg ( 𝐺 ∈ TarskiG → ( 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ↔ ( ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) ) ) )
33 32 biimpa ( ( 𝐺 ∈ TarskiG ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) → ( ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) ) )
34 33 adantrl ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) ) )
35 34 simpld ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( 𝑦 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) )
36 35 simprd ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → 𝑧 ∈ ( 𝑃pm ℝ ) )
37 31 36 jca ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) )
38 8 adantrr ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑦 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) ) ) )
39 38 simprd ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) ) )
40 39 simpld ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → dom 𝑥 = dom 𝑦 )
41 34 simprd ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) )
42 41 simpld ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → dom 𝑦 = dom 𝑧 )
43 40 42 eqtrd ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → dom 𝑥 = dom 𝑧 )
44 39 simprd ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
45 44 r19.21bi ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑥 ) → ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
46 45 r19.21bi ( ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑥 ) ∧ 𝑗 ∈ dom 𝑥 ) → ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
47 46 anasss ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) )
48 simpl ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) )
49 simprl ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → 𝑖 ∈ dom 𝑥 )
50 40 adantr ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → dom 𝑥 = dom 𝑦 )
51 49 50 eleqtrd ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → 𝑖 ∈ dom 𝑦 )
52 simprr ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → 𝑗 ∈ dom 𝑥 )
53 52 50 eleqtrd ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → 𝑗 ∈ dom 𝑦 )
54 41 simprd ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ∀ 𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) )
55 54 r19.21bi ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑦 ) → ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) )
56 55 r19.21bi ( ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑦 ) ∧ 𝑗 ∈ dom 𝑦 ) → ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) )
57 48 51 53 56 syl21anc ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → ( ( 𝑦𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) )
58 47 57 eqtrd ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) ) → ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) )
59 58 ralrimivva ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) )
60 43 59 jca ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( dom 𝑥 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) )
61 1 5 6 iscgrg ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑧 ↔ ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) ) ) )
62 61 adantr ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑧 ↔ ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑧 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑧𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧𝑗 ) ) ) ) ) )
63 37 60 62 mpbir2and ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → 𝑥 ( cgrG ‘ 𝐺 ) 𝑧 )
64 pm4.24 ( 𝑥 ∈ ( 𝑃pm ℝ ) ↔ ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) )
65 eqid dom 𝑥 = dom 𝑥
66 eqidd ( ( 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ) → ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) )
67 66 rgen2 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) )
68 65 67 pm3.2i ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) )
69 68 biantru ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) ↔ ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) ) ) )
70 64 69 bitri ( 𝑥 ∈ ( 𝑃pm ℝ ) ↔ ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) ) ) )
71 1 5 6 iscgrg ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑥 ∈ ( 𝑃pm ℝ ) ∧ 𝑥 ∈ ( 𝑃pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥 ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) = ( ( 𝑥𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥𝑗 ) ) ) ) ) )
72 70 71 bitr4id ( 𝐺 ∈ TarskiG → ( 𝑥 ∈ ( 𝑃pm ℝ ) ↔ 𝑥 ( cgrG ‘ 𝐺 ) 𝑥 ) )
73 4 29 63 72 iserd ( 𝐺 ∈ TarskiG → ( cgrG ‘ 𝐺 ) Er ( 𝑃pm ℝ ) )