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

Definition df-cgrg 25124
Description: Define the relation congruence bewteen shapes. Definition 4.4 of [Schwabhauser] p. 35. Ideally, we would define this for functions of any set, but we will used words (functions over ) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.)
Assertion
Ref Expression
df-cgrg cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))})
Distinct variable group:   𝑎,𝑏,𝑔,𝑖,𝑗

Detailed syntax breakdown of Definition df-cgrg
StepHypRef Expression
1 ccgrg 25123 . 2 class cgrG
2 vg . . 3 setvar 𝑔
3 cvv 3172 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1473 . . . . . . 7 class 𝑎
62cv 1473 . . . . . . . . 9 class 𝑔
7 cbs 15641 . . . . . . . . 9 class Base
86, 7cfv 5790 . . . . . . . 8 class (Base‘𝑔)
9 cr 9791 . . . . . . . 8 class
10 cpm 7722 . . . . . . . 8 class pm
118, 9, 10co 6527 . . . . . . 7 class ((Base‘𝑔) ↑pm ℝ)
125, 11wcel 1976 . . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
13 vb . . . . . . . 8 setvar 𝑏
1413cv 1473 . . . . . . 7 class 𝑏
1514, 11wcel 1976 . . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)
1612, 15wa 382 . . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
175cdm 5028 . . . . . . 7 class dom 𝑎
1814cdm 5028 . . . . . . 7 class dom 𝑏
1917, 18wceq 1474 . . . . . 6 wff dom 𝑎 = dom 𝑏
20 vi . . . . . . . . . . . 12 setvar 𝑖
2120cv 1473 . . . . . . . . . . 11 class 𝑖
2221, 5cfv 5790 . . . . . . . . . 10 class (𝑎𝑖)
23 vj . . . . . . . . . . . 12 setvar 𝑗
2423cv 1473 . . . . . . . . . . 11 class 𝑗
2524, 5cfv 5790 . . . . . . . . . 10 class (𝑎𝑗)
26 cds 15723 . . . . . . . . . . 11 class dist
276, 26cfv 5790 . . . . . . . . . 10 class (dist‘𝑔)
2822, 25, 27co 6527 . . . . . . . . 9 class ((𝑎𝑖)(dist‘𝑔)(𝑎𝑗))
2921, 14cfv 5790 . . . . . . . . . 10 class (𝑏𝑖)
3024, 14cfv 5790 . . . . . . . . . 10 class (𝑏𝑗)
3129, 30, 27co 6527 . . . . . . . . 9 class ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3228, 31wceq 1474 . . . . . . . 8 wff ((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3332, 23, 17wral 2895 . . . . . . 7 wff 𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3433, 20, 17wral 2895 . . . . . 6 wff 𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))
3519, 34wa 382 . . . . 5 wff (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗)))
3616, 35wa 382 . . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))
3736, 4, 13copab 4636 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))}
382, 3, 37cmpt 4637 . 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))})
391, 38wceq 1474 1 wff cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎𝑗 ∈ dom 𝑎((𝑎𝑖)(dist‘𝑔)(𝑎𝑗)) = ((𝑏𝑖)(dist‘𝑔)(𝑏𝑗))))})
Colors of variables: wff setvar class
This definition is referenced by:  iscgrg  25125  ercgrg  25130
  Copyright terms: Public domain W3C validator