Definition df-eqlg

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

	Ref	Expression
Assertion	df-eqlg	⊢ eqltrG = ( 𝑔 ∈ V ↦ { 𝑥 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ceqlg	⊢ eqltrG
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		cmap	⊢ ↑m
8		cc0	⊢ 0
9		cfzo	⊢ ..^
10		c3	⊢ 3
11	8 10 9	co	⊢ ( 0 ..^ 3 )
12	6 11 7	co	⊢ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) )
13	3	cv	⊢ 𝑥
14		ccgrg	⊢ cgrG
15	5 14	cfv	⊢ ( cgrG ‘ 𝑔 )
16		c1	⊢ 1
17	16 13	cfv	⊢ ( 𝑥 ‘ 1 )
18		c2	⊢ 2
19	18 13	cfv	⊢ ( 𝑥 ‘ 2 )
20	8 13	cfv	⊢ ( 𝑥 ‘ 0 )
21	17 19 20	cs3	⊢ ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩
22	13 21 15	wbr	⊢ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩
23	22 3 12	crab	⊢ { 𝑥 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ }
24	1 2 23	cmpt	⊢ ( 𝑔 ∈ V ↦ { 𝑥 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )
25	0 24	wceq	⊢ eqltrG = ( 𝑔 ∈ V ↦ { 𝑥 ∈ ( ( Base ‘ 𝑔 ) ↑m ( 0 ..^ 3 ) ) ∣ 𝑥 ( cgrG ‘ 𝑔 ) ⟨“ ( 𝑥 ‘ 1 ) ( 𝑥 ‘ 2 ) ( 𝑥 ‘ 0 ) ”⟩ } )