Definition df-cgrg 25406

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 NN) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.)

Assertion

Ref	Expression
df-cgrg	|- cgrG = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) } )

Distinct variable group:   a, b, g, i, j

Detailed syntax breakdown of Definition df-cgrg

Step	Hyp	Ref	Expression
1		ccgrg 25405	. 2 class cgrG
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . . . . . 8 setvar a
5	4	cv 1482	. . . . . . 7 class a
6	2	cv 1482	. . . . . . . . 9 class g
7		cbs 15857	. . . . . . . . 9 class Base
8	6, 7	cfv 5888	. . . . . . . 8 class ( Base ` g )
9		cr 9935	. . . . . . . 8 class RR
10		cpm 7858	. . . . . . . 8 class ^pm
11	8, 9, 10	co 6650	. . . . . . 7 class ( ( Base ` g ) ^pm RR )
12	5, 11	wcel 1990	. . . . . 6 wff a e. ( ( Base ` g ) ^pm RR )
13		vb	. . . . . . . 8 setvar b
14	13	cv 1482	. . . . . . 7 class b
15	14, 11	wcel 1990	. . . . . 6 wff b e. ( ( Base ` g ) ^pm RR )
16	12, 15	wa 384	. . . . 5 wff ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) )
17	5	cdm 5114	. . . . . . 7 class dom a
18	14	cdm 5114	. . . . . . 7 class dom b
19	17, 18	wceq 1483	. . . . . 6 wff dom a = dom b
20		vi	. . . . . . . . . . . 12 setvar i
21	20	cv 1482	. . . . . . . . . . 11 class i
22	21, 5	cfv 5888	. . . . . . . . . 10 class ( a ` i )
23		vj	. . . . . . . . . . . 12 setvar j
24	23	cv 1482	. . . . . . . . . . 11 class j
25	24, 5	cfv 5888	. . . . . . . . . 10 class ( a ` j )
26		cds 15950	. . . . . . . . . . 11 class dist
27	6, 26	cfv 5888	. . . . . . . . . 10 class ( dist ` g )
28	22, 25, 27	co 6650	. . . . . . . . 9 class ( ( a ` i ) ( dist ` g ) ( a ` j ) )
29	21, 14	cfv 5888	. . . . . . . . . 10 class ( b ` i )
30	24, 14	cfv 5888	. . . . . . . . . 10 class ( b ` j )
31	29, 30, 27	co 6650	. . . . . . . . 9 class ( ( b ` i ) ( dist ` g ) ( b ` j ) )
32	28, 31	wceq 1483	. . . . . . . 8 wff ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) )
33	32, 23, 17	wral 2912	. . . . . . 7 wff A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) )
34	33, 20, 17	wral 2912	. . . . . 6 wff A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) )
35	19, 34	wa 384	. . . . 5 wff ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) )
36	16, 35	wa 384	. . . 4 wff ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) )
37	36, 4, 13	copab 4712	. . 3 class { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) }
38	2, 3, 37	cmpt 4729	. 2 class ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) } )
39	1, 38	wceq 1483	1 wff cgrG = ( g e. _V |-> { <. a , b >. | ( ( a e. ( ( Base ` g ) ^pm RR ) /\ b e. ( ( Base ` g ) ^pm RR ) ) /\ ( dom a = dom b /\ A. i e. dom a A. j e. dom a ( ( a ` i ) ( dist ` g ) ( a ` j ) ) = ( ( b ` i ) ( dist ` g ) ( b ` j ) ) ) ) } )

This definition is referenced by:  iscgrg  25407  ercgrg  25412