Definition df-eqlg 25746

Description: Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019.)

Assertion

Ref	Expression
df-eqlg	|- eqltrG = ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) | x (cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )

Distinct variable group:   x, g

Detailed syntax breakdown of Definition df-eqlg

Step	Hyp	Ref	Expression
1		ceqlg 25745	. 2 class eqltrG
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vx	. . . . . 6 setvar x
5	4	cv 1482	. . . . 5 class x
6		c1 9937	. . . . . . 7 class 1
7	6, 5	cfv 5888	. . . . . 6 class ( x ` 1 )
8		c2 11070	. . . . . . 7 class 2
9	8, 5	cfv 5888	. . . . . 6 class ( x ` 2 )
10		cc0 9936	. . . . . . 7 class 0
11	10, 5	cfv 5888	. . . . . 6 class ( x ` 0 )
12	7, 9, 11	cs3 13587	. . . . 5 class <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) ">
13	2	cv 1482	. . . . . 6 class g
14		ccgrg 25405	. . . . . 6 class cgrG
15	13, 14	cfv 5888	. . . . 5 class (cgrG ` g )
16	5, 12, 15	wbr 4653	. . . 4 wff x (cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) ">
17		cbs 15857	. . . . . 6 class Base
18	13, 17	cfv 5888	. . . . 5 class ( Base ` g )
19		c3 11071	. . . . . 6 class 3
20		cfzo 12465	. . . . . 6 class ..^
21	10, 19, 20	co 6650	. . . . 5 class ( 0..^ 3 )
22		cmap 7857	. . . . 5 class ^m
23	18, 21, 22	co 6650	. . . 4 class ( ( Base ` g ) ^m ( 0..^ 3 ) )
24	16, 4, 23	crab 2916	. . 3 class { x e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) | x (cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> }
25	2, 3, 24	cmpt 4729	. 2 class ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) | x (cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
26	1, 25	wceq 1483	1 wff eqltrG = ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) | x (cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )

This definition is referenced by:  iseqlg  25747