MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-eqlg Structured version   Visualization version   GIF version

Definition df-eqlg 25546
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
StepHypRef Expression
1 ceqlg 25545 . 2 class eqltrG
2 vg . . 3 setvar 𝑔
3 cvv 3173 . . 3 class V
4 vx . . . . . 6 setvar 𝑥
54cv 1474 . . . . 5 class 𝑥
6 c1 9816 . . . . . . 7 class 1
76, 5cfv 5804 . . . . . 6 class (𝑥‘1)
8 c2 10947 . . . . . . 7 class 2
98, 5cfv 5804 . . . . . 6 class (𝑥‘2)
10 cc0 9815 . . . . . . 7 class 0
1110, 5cfv 5804 . . . . . 6 class (𝑥‘0)
127, 9, 11cs3 13438 . . . . 5 class ⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
132cv 1474 . . . . . 6 class 𝑔
14 ccgrg 25205 . . . . . 6 class cgrG
1513, 14cfv 5804 . . . . 5 class (cgrG‘𝑔)
165, 12, 15wbr 4583 . . . 4 wff 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩
17 cbs 15695 . . . . . 6 class Base
1813, 17cfv 5804 . . . . 5 class (Base‘𝑔)
19 c3 10948 . . . . . 6 class 3
20 cfzo 12334 . . . . . 6 class ..^
2110, 19, 20co 6549 . . . . 5 class (0..^3)
22 cmap 7744 . . . . 5 class 𝑚
2318, 21, 22co 6549 . . . 4 class ((Base‘𝑔) ↑𝑚 (0..^3))
2416, 4, 23crab 2900 . . 3 class {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩}
252, 3, 24cmpt 4643 . 2 class (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
261, 25wceq 1475 1 wff eqltrG = (𝑔 ∈ V ↦ {𝑥 ∈ ((Base‘𝑔) ↑𝑚 (0..^3)) ∣ 𝑥(cgrG‘𝑔)⟨“(𝑥‘1)(𝑥‘2)(𝑥‘0)”⟩})
Colors of variables: wff setvar class
This definition is referenced by:  iseqlg  25547
  Copyright terms: Public domain W3C validator