Metamath Proof Explorer

Theorem grpidval

Description: The value of the identity element of a group. (Contributed by NM, 20-Aug-2011) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses grpidval.b 
|- B = ( Base ` G )
grpidval.p 
|- .+ = ( +g ` G )
grpidval.o 
|- .0. = ( 0g ` G )
Assertion grpidval 
|- .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )

Proof

Step Hyp Ref Expression
1 grpidval.b 
 |-  B = ( Base ` G )
2 grpidval.p 
 |-  .+ = ( +g ` G )
3 grpidval.o 
 |-  .0. = ( 0g ` G )
4 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
5 4 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = B )
6 5 eleq2d 
 |-  ( g = G -> ( e e. ( Base ` g ) <-> e e. B ) )
7 fveq2 
 |-  ( g = G -> ( +g ` g ) = ( +g ` G ) )
8 7 2 eqtr4di 
 |-  ( g = G -> ( +g ` g ) = .+ )
9 8 oveqd 
 |-  ( g = G -> ( e ( +g ` g ) x ) = ( e .+ x ) )
10 9 eqeq1d 
 |-  ( g = G -> ( ( e ( +g ` g ) x ) = x <-> ( e .+ x ) = x ) )
11 8 oveqd 
 |-  ( g = G -> ( x ( +g ` g ) e ) = ( x .+ e ) )
12 11 eqeq1d 
 |-  ( g = G -> ( ( x ( +g ` g ) e ) = x <-> ( x .+ e ) = x ) )
13 10 12 anbi12d 
 |-  ( g = G -> ( ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) <-> ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
14 5 13 raleqbidv 
 |-  ( g = G -> ( A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) <-> A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
15 6 14 anbi12d 
 |-  ( g = G -> ( ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) <-> ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) )
16 15 iotabidv 
 |-  ( g = G -> ( iota e ( e e. ( Base ` g ) /\ A. x e. ( Base ` g ) ( ( e ( +g ` g ) x ) = x /\ ( x ( +g ` g ) e ) = x ) ) ) = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) )
17 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 ) ) ) )
18 iotaex 
 |-  ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) e. _V
19 16 17 18 fvmpt 
 |-  ( G e. _V -> ( 0g ` G ) = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) )
20 fvprc 
 |-  ( -. G e. _V -> ( 0g ` G ) = (/) )
21 euex 
 |-  ( E! e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) -> E. e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
22 n0i 
 |-  ( e e. B -> -. B = (/) )
23 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
24 1 23 eqtrid 
 |-  ( -. G e. _V -> B = (/) )
25 22 24 nsyl2 
 |-  ( e e. B -> G e. _V )
26 25 adantr 
 |-  ( ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) -> G e. _V )
27 26 exlimiv 
 |-  ( E. e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) -> G e. _V )
28 21 27 syl 
 |-  ( E! e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) -> G e. _V )
29 iotanul 
 |-  ( -. E! e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) -> ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) = (/) )
30 28 29 nsyl5 
 |-  ( -. G e. _V -> ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) = (/) )
31 20 30 eqtr4d 
 |-  ( -. G e. _V -> ( 0g ` G ) = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) ) )
32 19 31 pm2.61i 
 |-  ( 0g ` G ) = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
33 3 32 eqtri 
 |-  .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )