MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ercgrg Structured version   Visualization version   GIF version

Theorem ercgrg 27697
Description: The shape congruence relation is an equivalence relation. Statement 4.4 of [Schwabhauser] p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019.)
Hypothesis
Ref Expression
ercgrg.p 𝑃 = (Base‘𝐺)
Assertion
Ref Expression
ercgrg (𝐺 ∈ TarskiG → (cgrG‘𝐺) Er (𝑃pm ℝ))

Proof of Theorem ercgrg
Dummy variables 𝑎 𝑏 𝑔 𝑖 𝑗 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cgrg 27691 . . . 4 cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))})
21relmptopab 7640 . . 3 Rel (cgrG‘𝐺)
32a1i 11 . 2 (𝐺 ∈ TarskiG → Rel (cgrG‘𝐺))
4 ercgrg.p . . . . . . 7 𝑃 = (Base‘𝐺)
5 eqid 2732 . . . . . . 7 (dist‘𝐺) = (dist‘𝐺)
6 eqid 2732 . . . . . . 7 (cgrG‘𝐺) = (cgrG‘𝐺)
74, 5, 6iscgrg 27692 . . . . . 6 (𝐺 ∈ TarskiG → (𝑥(cgrG‘𝐺)𝑦 ↔ ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑦 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑦 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗))))))
87biimpa 477 . . . . 5 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑦 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑦 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))))
98simpld 495 . . . 4 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → (𝑥 ∈ (𝑃pm ℝ) ∧ 𝑦 ∈ (𝑃pm ℝ)))
109ancomd 462 . . 3 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → (𝑦 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)))
118simprd 496 . . . . . 6 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → (dom 𝑥 = dom 𝑦 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗))))
1211simpld 495 . . . . 5 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → dom 𝑥 = dom 𝑦)
1312eqcomd 2738 . . . 4 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → dom 𝑦 = dom 𝑥)
14 simpl 483 . . . . . . 7 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → (𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦))
15 simprl 769 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → 𝑖 ∈ dom 𝑦)
1612adantr 481 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → dom 𝑥 = dom 𝑦)
1715, 16eleqtrrd 2836 . . . . . . 7 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → 𝑖 ∈ dom 𝑥)
18 simprr 771 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → 𝑗 ∈ dom 𝑦)
1918, 16eleqtrrd 2836 . . . . . . 7 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → 𝑗 ∈ dom 𝑥)
2011simprd 496 . . . . . . . . 9 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
2120r19.21bi 3248 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ 𝑖 ∈ dom 𝑥) → ∀𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
2221r19.21bi 3248 . . . . . . 7 ((((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ 𝑖 ∈ dom 𝑥) ∧ 𝑗 ∈ dom 𝑥) → ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
2314, 17, 19, 22syl21anc 836 . . . . . 6 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
2423eqcomd 2738 . . . . 5 (((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) ∧ (𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦)) → ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)))
2524ralrimivva 3200 . . . 4 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)))
2613, 25jca 512 . . 3 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → (dom 𝑦 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗))))
274, 5, 6iscgrg 27692 . . . 4 (𝐺 ∈ TarskiG → (𝑦(cgrG‘𝐺)𝑥 ↔ ((𝑦 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)) ∧ (dom 𝑦 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗))))))
2827adantr 481 . . 3 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → (𝑦(cgrG‘𝐺)𝑥 ↔ ((𝑦 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)) ∧ (dom 𝑦 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗))))))
2910, 26, 28mpbir2and 711 . 2 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → 𝑦(cgrG‘𝐺)𝑥)
309simpld 495 . . . . 5 ((𝐺 ∈ TarskiG ∧ 𝑥(cgrG‘𝐺)𝑦) → 𝑥 ∈ (𝑃pm ℝ))
3130adantrr 715 . . . 4 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → 𝑥 ∈ (𝑃pm ℝ))
324, 5, 6iscgrg 27692 . . . . . . . 8 (𝐺 ∈ TarskiG → (𝑦(cgrG‘𝐺)𝑧 ↔ ((𝑦 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)) ∧ (dom 𝑦 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗))))))
3332biimpa 477 . . . . . . 7 ((𝐺 ∈ TarskiG ∧ 𝑦(cgrG‘𝐺)𝑧) → ((𝑦 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)) ∧ (dom 𝑦 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))))
3433adantrl 714 . . . . . 6 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → ((𝑦 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)) ∧ (dom 𝑦 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))))
3534simpld 495 . . . . 5 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → (𝑦 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)))
3635simprd 496 . . . 4 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → 𝑧 ∈ (𝑃pm ℝ))
3731, 36jca 512 . . 3 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → (𝑥 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)))
388adantrr 715 . . . . . . 7 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑦 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑦 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))))
3938simprd 496 . . . . . 6 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → (dom 𝑥 = dom 𝑦 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗))))
4039simpld 495 . . . . 5 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → dom 𝑥 = dom 𝑦)
4134simprd 496 . . . . . 6 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → (dom 𝑦 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗))))
4241simpld 495 . . . . 5 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → dom 𝑦 = dom 𝑧)
4340, 42eqtrd 2772 . . . 4 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → dom 𝑥 = dom 𝑧)
4439simprd 496 . . . . . . . . 9 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
4544r19.21bi 3248 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ 𝑖 ∈ dom 𝑥) → ∀𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
4645r19.21bi 3248 . . . . . . 7 ((((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ 𝑖 ∈ dom 𝑥) ∧ 𝑗 ∈ dom 𝑥) → ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
4746anasss 467 . . . . . 6 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)))
48 simpl 483 . . . . . . 7 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → (𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)))
49 simprl 769 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → 𝑖 ∈ dom 𝑥)
5040adantr 481 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → dom 𝑥 = dom 𝑦)
5149, 50eleqtrd 2835 . . . . . . 7 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → 𝑖 ∈ dom 𝑦)
52 simprr 771 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → 𝑗 ∈ dom 𝑥)
5352, 50eleqtrd 2835 . . . . . . 7 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → 𝑗 ∈ dom 𝑦)
5441simprd 496 . . . . . . . . 9 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → ∀𝑖 ∈ dom 𝑦𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))
5554r19.21bi 3248 . . . . . . . 8 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ 𝑖 ∈ dom 𝑦) → ∀𝑗 ∈ dom 𝑦((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))
5655r19.21bi 3248 . . . . . . 7 ((((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ 𝑖 ∈ dom 𝑦) ∧ 𝑗 ∈ dom 𝑦) → ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))
5748, 51, 53, 56syl21anc 836 . . . . . 6 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → ((𝑦𝑖)(dist‘𝐺)(𝑦𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))
5847, 57eqtrd 2772 . . . . 5 (((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) ∧ (𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥)) → ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))
5958ralrimivva 3200 . . . 4 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗)))
6043, 59jca 512 . . 3 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → (dom 𝑥 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗))))
614, 5, 6iscgrg 27692 . . . 4 (𝐺 ∈ TarskiG → (𝑥(cgrG‘𝐺)𝑧 ↔ ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗))))))
6261adantr 481 . . 3 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → (𝑥(cgrG‘𝐺)𝑧 ↔ ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑧 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑧 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑧𝑖)(dist‘𝐺)(𝑧𝑗))))))
6337, 60, 62mpbir2and 711 . 2 ((𝐺 ∈ TarskiG ∧ (𝑥(cgrG‘𝐺)𝑦𝑦(cgrG‘𝐺)𝑧)) → 𝑥(cgrG‘𝐺)𝑧)
64 pm4.24 564 . . . 4 (𝑥 ∈ (𝑃pm ℝ) ↔ (𝑥 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)))
65 eqid 2732 . . . . . 6 dom 𝑥 = dom 𝑥
66 eqidd 2733 . . . . . . 7 ((𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥) → ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)))
6766rgen2 3197 . . . . . 6 𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗))
6865, 67pm3.2i 471 . . . . 5 (dom 𝑥 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)))
6968biantru 530 . . . 4 ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)) ↔ ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)))))
7064, 69bitri 274 . . 3 (𝑥 ∈ (𝑃pm ℝ) ↔ ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)))))
714, 5, 6iscgrg 27692 . . 3 (𝐺 ∈ TarskiG → (𝑥(cgrG‘𝐺)𝑥 ↔ ((𝑥 ∈ (𝑃pm ℝ) ∧ 𝑥 ∈ (𝑃pm ℝ)) ∧ (dom 𝑥 = dom 𝑥 ∧ ∀𝑖 ∈ dom 𝑥𝑗 ∈ dom 𝑥((𝑥𝑖)(dist‘𝐺)(𝑥𝑗)) = ((𝑥𝑖)(dist‘𝐺)(𝑥𝑗))))))
7270, 71bitr4id 289 . 2 (𝐺 ∈ TarskiG → (𝑥 ∈ (𝑃pm ℝ) ↔ 𝑥(cgrG‘𝐺)𝑥))
733, 29, 63, 72iserd 8714 1 (𝐺 ∈ TarskiG → (cgrG‘𝐺) Er (𝑃pm ℝ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3061  Vcvv 3474   class class class wbr 5142  dom cdm 5670  Rel wrel 5675  cfv 6533  (class class class)co 7394   Er wer 8685  pm cpm 8806  cr 11093  Basecbs 17128  distcds 17190  TarskiGcstrkg 27607  cgrGccgrg 27690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6485  df-fun 6535  df-fv 6541  df-ov 7397  df-er 8688  df-cgrg 27691
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator