Metamath Proof Explorer

Definition df-eqlg

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceqlg 
 |-  eqltrG
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 cmap 
 |-  ^m
8 cc0 
 |-  0
9 cfzo 
 |-  ..^
10 c3 
 |-  3
11 8 10 9 co 
 |-  ( 0 ..^ 3 )
12 6 11 7 co 
 |-  ( ( Base ` g ) ^m ( 0 ..^ 3 ) )
13 3 cv 
 |-  x
14 ccgrg 
 |-  cgrG
15 5 14 cfv 
 |-  ( cgrG ` g )
16 c1 
 |-  1
17 16 13 cfv 
 |-  ( x ` 1 )
18 c2 
 |-  2
19 18 13 cfv 
 |-  ( x ` 2 )
20 8 13 cfv 
 |-  ( x ` 0 )
21 17 19 20 cs3 
 |-  <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) ">
22 13 21 15 wbr 
 |-  x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) ">
23 22 3 12 crab 
 |-  { x e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) | x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> }
24 1 2 23 cmpt 
 |-  ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) | x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )
25 0 24 wceq 
 |-  eqltrG = ( g e. _V |-> { x e. ( ( Base ` g ) ^m ( 0 ..^ 3 ) ) | x ( cgrG ` g ) <" ( x ` 1 ) ( x ` 2 ) ( x ` 0 ) "> } )