Definition df-0g 17486

Description: Define group identity element. Remark: this definition is required here because the symbol 0_g is already used in df-gsum 17487. The related theorems are provided later, see grpidval 18674. (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

Step	Hyp	Ref	Expression
1		c0g 17484	. 2 class 0g
2		vg	. . 3 setvar 𝑔
3		cvv 3480	. . 3 class V
4		ve	. . . . . . 7 setvar 𝑒
5	4	cv 1539	. . . . . 6 class 𝑒
6	2	cv 1539	. . . . . . 7 class 𝑔
7		cbs 17247	. . . . . . 7 class Base
8	6, 7	cfv 6561	. . . . . 6 class (Base‘𝑔)
9	5, 8	wcel 2108	. . . . 5 wff 𝑒 ∈ (Base‘𝑔)
10		vx	. . . . . . . . . 10 setvar 𝑥
11	10	cv 1539	. . . . . . . . 9 class 𝑥
12		cplusg 17297	. . . . . . . . . 10 class +g
13	6, 12	cfv 6561	. . . . . . . . 9 class (+g‘𝑔)
14	5, 11, 13	co 7431	. . . . . . . 8 class (𝑒(+g‘𝑔)𝑥)
15	14, 11	wceq 1540	. . . . . . 7 wff (𝑒(+g‘𝑔)𝑥) = 𝑥
16	11, 5, 13	co 7431	. . . . . . . 8 class (𝑥(+g‘𝑔)𝑒)
17	16, 11	wceq 1540	. . . . . . 7 wff (𝑥(+g‘𝑔)𝑒) = 𝑥
18	15, 17	wa 395	. . . . . 6 wff ((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)
19	18, 10, 8	wral 3061	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)
20	9, 19	wa 395	. . . 4 wff (𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))
21	20, 4	cio 6512	. . 3 class (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))
22	2, 3, 21	cmpt 5225	. 2 class (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))))
23	1, 22	wceq 1540	1 wff 0g = (𝑔 ∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))))

This definition is referenced by:  grpidval  18674  fn0g  18676