Definition df-eqlg 26215

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

Assertion

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

Distinct variable group:   𝑥,𝑔

Detailed syntax breakdown of Definition df-eqlg

Step	Hyp	Ref	Expression
1		ceqlg 26214	. 2 class eqltrG
2		vg	. . 3 setvar 𝑔
3		cvv 3397	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1600	. . . . 5 class 𝑥
6		c1 10273	. . . . . . 7 class 1
7	6, 5	cfv 6135	. . . . . 6 class (𝑥‘1)
8		c2 11430	. . . . . . 7 class 2
9	8, 5	cfv 6135	. . . . . 6 class (𝑥‘2)
10		cc0 10272	. . . . . . 7 class 0
11	10, 5	cfv 6135	. . . . . 6 class (𝑥‘0)
12	7, 9, 11	cs3 13993	. . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
13	2	cv 1600	. . . . . 6 class 𝑔
14		ccgrg 25861	. . . . . 6 class cgrG
15	13, 14	cfv 6135	. . . . 5 class (cgrG‘𝑔)
16	5, 12, 15	wbr 4886	. . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17		cbs 16255	. . . . . 6 class Base
18	13, 17	cfv 6135	. . . . 5 class (Base‘𝑔)
19		c3 11431	. . . . . 6 class 3
20		cfzo 12784	. . . . . 6 class ..^
21	10, 19, 20	co 6922	. . . . 5 class (0..^3)
22		cmap 8140	. . . . 5 class ↑𝑚
23	18, 21, 22	co 6922	. . . 4 class ((Base‘𝑔) ↑𝑚 (0..^3))
24	16, 4, 23	crab 3093	. . 3 class {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
25	2, 3, 24	cmpt 4965	. 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
26	1, 25	wceq 1601	1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})

This definition is referenced by:  iseqlg  26216