This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-0g

Description: Define group identity element. Remark: this definition is required here because the symbol 0g is already used in df-gsum . The related theorems are provided later, see grpidval . (Contributed by NM, 20-Aug-2011)

Ref Expression
Assertion df-0g ⊢ 0 𝑔 = g ∈ V ⟼ ι e | e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0g class 0 𝑔
1 vg setvar g
2 cvv class V
3 ve setvar e
4 3 cv setvar e
5 cbs class Base
6 1 cv setvar g
7 6 5 cfv class Base g
8 4 7 wcel wff e ∈ Base g
9 vx setvar x
10 cplusg class + 𝑔
11 6 10 cfv class + g
12 9 cv setvar x
13 4 12 11 co class e + g x
14 13 12 wceq wff e + g x = x
15 12 4 11 co class x + g e
16 15 12 wceq wff x + g e = x
17 14 16 wa wff e + g x = x ∧ x + g e = x
18 17 9 7 wral wff ∀ x ∈ Base g e + g x = x ∧ x + g e = x
19 8 18 wa wff e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x
20 19 3 cio class ι e | e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x
21 1 2 20 cmpt class g ∈ V ⟼ ι e | e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x
22 0 21 wceq wff 0 𝑔 = g ∈ V ⟼ ι e | e ∈ Base g ∧ ∀ x ∈ Base g e + g x = x ∧ x + g e = x