Definition df-0g 12575

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

Assertion

Ref	Expression
df-0g	|- 0g = ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )

Distinct variable group:   e, g, x

Detailed syntax breakdown of Definition df-0g

Step	Hyp	Ref	Expression
1		c0g 12573	. 2 class 0g
2		vg	. . 3 setvar g
3		cvv 2726	. . 3 class _V
4		ve	. . . . . . 7 setvar e
5	4	cv 1342	. . . . . 6 class e
6	2	cv 1342	. . . . . . 7 class g
7		cbs 12394	. . . . . . 7 class Base
8	6, 7	cfv 5188	. . . . . 6 class ( Base ` g )
9	5, 8	wcel 2136	. . . . 5 wff e e. ( Base ` g )
10		vx	. . . . . . . . . 10 setvar x
11	10	cv 1342	. . . . . . . . 9 class x
12		cplusg 12457	. . . . . . . . . 10 class +g
13	6, 12	cfv 5188	. . . . . . . . 9 class ( +g ` g )
14	5, 11, 13	co 5842	. . . . . . . 8 class ( e ( +g ` g ) x )
15	14, 11	wceq 1343	. . . . . . 7 wff ( e ( +g ` g ) x ) = x
16	11, 5, 13	co 5842	. . . . . . . 8 class ( x ( +g ` g ) e )
17	16, 11	wceq 1343	. . . . . . 7 wff ( x ( +g ` g ) e ) = x
18	15, 17	wa 103	. . . . . 6 wff ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x )
19	18, 10, 8	wral 2444	. . . . 5 wff A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x )
20	9, 19	wa 103	. . . 4 wff ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) )
21	20, 4	cio 5151	. . 3 class ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) )
22	2, 3, 21	cmpt 4043	. 2 class ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )
23	1, 22	wceq 1343	1 wff 0g = ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )

This definition is referenced by:  grpidvalg  12604  fn0g  12606