Definition df-cgrg 25206

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

Step	Hyp	Ref	Expression
1		ccgrg 25205	. 2 class cgrG
2		vg	. . 3 setvar 𝑔
3		cvv 3173	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1474	. . . . . . 7 class 𝑎
6	2	cv 1474	. . . . . . . . 9 class 𝑔
7		cbs 15695	. . . . . . . . 9 class Base
8	6, 7	cfv 5804	. . . . . . . 8 class (Base‘𝑔)
9		cr 9814	. . . . . . . 8 class ℝ
10		cpm 7745	. . . . . . . 8 class ↑pm
11	8, 9, 10	co 6549	. . . . . . 7 class ((Base‘𝑔) ↑pm ℝ)
12	5, 11	wcel 1977	. . . . . 6 wff 𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
13		vb	. . . . . . . 8 setvar 𝑏
14	13	cv 1474	. . . . . . 7 class 𝑏
15	14, 11	wcel 1977	. . . . . 6 wff 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)
16	12, 15	wa 383	. . . . 5 wff (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
17	5	cdm 5038	. . . . . . 7 class dom 𝑎
18	14	cdm 5038	. . . . . . 7 class dom 𝑏
19	17, 18	wceq 1475	. . . . . 6 wff dom 𝑎 = dom 𝑏
20		vi	. . . . . . . . . . . 12 setvar 𝑖
21	20	cv 1474	. . . . . . . . . . 11 class 𝑖
22	21, 5	cfv 5804	. . . . . . . . . 10 class (𝑎‘𝑖)
23		vj	. . . . . . . . . . . 12 setvar 𝑗
24	23	cv 1474	. . . . . . . . . . 11 class 𝑗
25	24, 5	cfv 5804	. . . . . . . . . 10 class (𝑎‘𝑗)
26		cds 15777	. . . . . . . . . . 11 class dist
27	6, 26	cfv 5804	. . . . . . . . . 10 class (dist‘𝑔)
28	22, 25, 27	co 6549	. . . . . . . . 9 class ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗))
29	21, 14	cfv 5804	. . . . . . . . . 10 class (𝑏‘𝑖)
30	24, 14	cfv 5804	. . . . . . . . . 10 class (𝑏‘𝑗)
31	29, 30, 27	co 6549	. . . . . . . . 9 class ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
32	28, 31	wceq 1475	. . . . . . . 8 wff ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
33	32, 23, 17	wral 2896	. . . . . . 7 wff ∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
34	33, 20, 17	wral 2896	. . . . . 6 wff ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))
35	19, 34	wa 383	. . . . 5 wff (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))
36	16, 35	wa 383	. . . 4 wff ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))
37	36, 4, 13	copab 4642	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}
38	2, 3, 37	cmpt 4643	. 2 class (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})
39	1, 38	wceq 1475	1 wff cgrG = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))})

This definition is referenced by:  iscgrg  25207  ercgrg  25212