Definition df-cgra 25700

Description: Define the congruence relation bewteen angles. As for triangles we use "words of points". See iscgra 25701 for a more human readable version. (Contributed by Thierry Arnoux, 30-Jul-2020.)

Assertion

Ref	Expression
df-cgra	|- cgrA = ( g e. _V |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )

Distinct variable group:   a, b, g, k, p, x, y

Detailed syntax breakdown of Definition df-cgra

Step	Hyp	Ref	Expression
1		ccgra 25699	. 2 class cgrA
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . . . . . . . 10 setvar a
5	4	cv 1482	. . . . . . . . 9 class a
6		vp	. . . . . . . . . . 11 setvar p
7	6	cv 1482	. . . . . . . . . 10 class p
8		cc0 9936	. . . . . . . . . . 11 class 0
9		c3 11071	. . . . . . . . . . 11 class 3
10		cfzo 12465	. . . . . . . . . . 11 class ..^
11	8, 9, 10	co 6650	. . . . . . . . . 10 class ( 0..^ 3 )
12		cmap 7857	. . . . . . . . . 10 class ^m
13	7, 11, 12	co 6650	. . . . . . . . 9 class ( p ^m ( 0..^ 3 ) )
14	5, 13	wcel 1990	. . . . . . . 8 wff a e. ( p ^m ( 0..^ 3 ) )
15		vb	. . . . . . . . . 10 setvar b
16	15	cv 1482	. . . . . . . . 9 class b
17	16, 13	wcel 1990	. . . . . . . 8 wff b e. ( p ^m ( 0..^ 3 ) )
18	14, 17	wa 384	. . . . . . 7 wff ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) )
19		vx	. . . . . . . . . . . . 13 setvar x
20	19	cv 1482	. . . . . . . . . . . 12 class x
21		c1 9937	. . . . . . . . . . . . 13 class 1
22	21, 16	cfv 5888	. . . . . . . . . . . 12 class ( b ` 1 )
23		vy	. . . . . . . . . . . . 13 setvar y
24	23	cv 1482	. . . . . . . . . . . 12 class y
25	20, 22, 24	cs3 13587	. . . . . . . . . . 11 class <" x ( b ` 1 ) y ">
26	2	cv 1482	. . . . . . . . . . . 12 class g
27		ccgrg 25405	. . . . . . . . . . . 12 class cgrG
28	26, 27	cfv 5888	. . . . . . . . . . 11 class (cgrG ` g )
29	5, 25, 28	wbr 4653	. . . . . . . . . 10 wff a (cgrG ` g ) <" x ( b ` 1 ) y ">
30	8, 16	cfv 5888	. . . . . . . . . . 11 class ( b ` 0 )
31		vk	. . . . . . . . . . . . 13 setvar k
32	31	cv 1482	. . . . . . . . . . . 12 class k
33	22, 32	cfv 5888	. . . . . . . . . . 11 class ( k ` ( b ` 1 ) )
34	20, 30, 33	wbr 4653	. . . . . . . . . 10 wff x ( k ` ( b ` 1 ) ) ( b ` 0 )
35		c2 11070	. . . . . . . . . . . 12 class 2
36	35, 16	cfv 5888	. . . . . . . . . . 11 class ( b ` 2 )
37	24, 36, 33	wbr 4653	. . . . . . . . . 10 wff y ( k ` ( b ` 1 ) ) ( b ` 2 )
38	29, 34, 37	w3a 1037	. . . . . . . . 9 wff ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) )
39	38, 23, 7	wrex 2913	. . . . . . . 8 wff E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) )
40	39, 19, 7	wrex 2913	. . . . . . 7 wff E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) )
41	18, 40	wa 384	. . . . . 6 wff ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) )
42		chlg 25495	. . . . . . 7 class hlG
43	26, 42	cfv 5888	. . . . . 6 class (hlG ` g )
44	41, 31, 43	wsbc 3435	. . . . 5 wff [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) )
45		cbs 15857	. . . . . 6 class Base
46	26, 45	cfv 5888	. . . . 5 class ( Base ` g )
47	44, 6, 46	wsbc 3435	. . . 4 wff [. ( Base ` g ) / p ]. [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) )
48	47, 4, 15	copab 4712	. . 3 class { <. a , b >. | [. ( Base ` g ) / p ]. [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) }
49	2, 3, 48	cmpt 4729	. 2 class ( g e. _V |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
50	1, 49	wceq 1483	1 wff cgrA = ( g e. _V |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. (hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0..^ 3 ) ) /\ b e. ( p ^m ( 0..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a (cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )

This definition is referenced by:  iscgra  25701