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 1 5 6 iscgrg ⊢ ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) ) )
65 pm4.24 ⊢ ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ↔ ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) )
66 eqid ⊢ dom 𝑥 = dom 𝑥
67 eqidd ⊢ ( ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) )
68 67 rgen2 ⊢ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) )
69 66 68 pm3.2i ⊢ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) )
70 69 biantru ⊢ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) )
71 65 70 bitri ⊢ ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) )
72 64 71 syl6rbbr ⊢ ( 𝐺 ∈ TarskiG → ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ↔ 𝑥 ( cgrG ‘ 𝐺 ) 𝑥 ) )
73 4 29 63 72 iserd ⊢ ( 𝐺 ∈ TarskiG → ( cgrG ‘ 𝐺 ) Er ( 𝑃 ↑pm ℝ ) )