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

Definition df-0g 17161
Description: Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum 17162. The related theorems are provided later, see grpidval 18354. (Contributed by NM, 20-Aug-2011.)
Assertion
Ref Expression
df-0g 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥))))
Distinct variable group:   𝑒,𝑔,𝑥

Detailed syntax breakdown of Definition df-0g
StepHypRef Expression
1 c0g 17159 . 2 class 0g
2 vg . . 3 setvar 𝑔
3 cvv 3433 . . 3 class V
4 ve . . . . . . 7 setvar 𝑒
54cv 1538 . . . . . 6 class 𝑒
62cv 1538 . . . . . . 7 class 𝑔
7 cbs 16921 . . . . . . 7 class Base
86, 7cfv 6437 . . . . . 6 class (Base‘𝑔)
95, 8wcel 2107 . . . . 5 wff 𝑒 ∈ (Base‘𝑔)
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1538 . . . . . . . . 9 class 𝑥
12 cplusg 16971 . . . . . . . . . 10 class +g
136, 12cfv 6437 . . . . . . . . 9 class (+g𝑔)
145, 11, 13co 7284 . . . . . . . 8 class (𝑒(+g𝑔)𝑥)
1514, 11wceq 1539 . . . . . . 7 wff (𝑒(+g𝑔)𝑥) = 𝑥
1611, 5, 13co 7284 . . . . . . . 8 class (𝑥(+g𝑔)𝑒)
1716, 11wceq 1539 . . . . . . 7 wff (𝑥(+g𝑔)𝑒) = 𝑥
1815, 17wa 396 . . . . . 6 wff ((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥)
1918, 10, 8wral 3065 . . . . 5 wff 𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥)
209, 19wa 396 . . . 4 wff (𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥))
2120, 4cio 6393 . . 3 class (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥)))
222, 3, 21cmpt 5158 . 2 class (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥))))
231, 22wceq 1539 1 wff 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g𝑔)𝑥) = 𝑥 ∧ (𝑥(+g𝑔)𝑒) = 𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  grpidval  18354  fn0g  18356
  Copyright terms: Public domain W3C validator