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 
|- 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 ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0g 
 |-  0g
1 vg 
 |-  g
2 cvv 
 |-  _V
3 ve 
 |-  e
4 3 cv 
 |-  e
5 cbs 
 |-  Base
6 1 cv 
 |-  g
7 6 5 cfv 
 |-  ( Base ` g )
8 4 7 wcel 
 |-  e e. ( Base ` g )
9 vx 
 |-  x
10 cplusg 
 |-  +g
11 6 10 cfv 
 |-  ( +g ` g )
12 9 cv 
 |-  x
13 4 12 11 co 
 |-  ( e ( +g ` g ) x )
14 13 12 wceq 
 |-  ( e ( +g ` g ) x ) = x
15 12 4 11 co 
 |-  ( x ( +g ` g ) e )
16 15 12 wceq 
 |-  ( x ( +g ` g ) e ) = x
17 14 16 wa 
 |-  ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x )
18 17 9 7 wral 
 |-  A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x )
19 8 18 wa 
 |-  ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) )
20 19 3 cio 
 |-  ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) )
21 1 2 20 cmpt 
 |-  ( g e. _V |-> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) )
22 0 21 wceq 
 |-  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 ) ) ) )