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_{𝑔}=\left(g\in \mathrm{V}⟼\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0g	$$class{0}_{𝑔}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		ve	$$setvare$$
4	3	cv	$$setvare$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvarg$$
7	6 5	cfv	$$class{\mathrm{Base}}_g$$
8	4 7	wcel	$$wffe\in {\mathrm{Base}}_g$$
9		vx	$$setvarx$$
10		cplusg	$$class{+}_{𝑔}$$
11	6 10	cfv	$$class{+}_g$$
12	9	cv	$$setvarx$$
13	4 12 11	co	$$class\left(e{+}_{g}x\right)$$
14	13 12	wceq	$$wffe{+}_{g}x=x$$
15	12 4 11	co	$$class\left(x{+}_{g}e\right)$$
16	15 12	wceq	$$wffx{+}_{g}e=x$$
17	14 16	wa	$$wff\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)$$
18	17 9 7	wral	$$wff\forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)$$
19	8 18	wa	$$wff\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)$$
20	19 3	cio	$$class\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)$$
21	1 2 20	cmpt	$$class\left(g\in \mathrm{V}⟼\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)\right)$$
22	0 21	wceq	$$wff{0}_{𝑔}=\left(g\in \mathrm{V}⟼\left(\iota e|\left(e\in {\mathrm{Base}}_g\wedge \forall x\in {\mathrm{Base}}_g\left(e{+}_{g}x=x\wedge x{+}_{g}e=x\right)\right)\right)\right)$$