Metamath Proof Explorer

Theorem 0gisid

Description: In a structure with an identity element, the group identity element is an identity element of the structure. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 11-Aug-2026)

Ref Expression
Hypotheses ismgmid.b 
|- B = ( Base ` G )
ismgmid.o 
|- .0. = ( 0g ` G )
ismgmid.p 
|- .+ = ( +g ` G )
mgmidcl.e 
|- ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
Assertion 0gisid 
|- ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )

Proof

Step Hyp Ref Expression
1 ismgmid.b 
 |-  B = ( Base ` G )
2 ismgmid.o 
 |-  .0. = ( 0g ` G )
3 ismgmid.p 
 |-  .+ = ( +g ` G )
4 mgmidcl.e 
 |-  ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
5 oveq1 
 |-  ( e = i -> ( e .+ x ) = ( i .+ x ) )
6 5 eqeq1d 
 |-  ( e = i -> ( ( e .+ x ) = x <-> ( i .+ x ) = x ) )
7 6 ovanraleqv 
 |-  ( e = i -> ( A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) )
8 7 cbvrexvw 
 |-  ( E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> E. i e. B A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) )
9 1 2 3 4 ismgmid 
 |-  ( ph -> ( ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) <-> .0. = i ) )
10 9 biimpa 
 |-  ( ( ph /\ ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) ) -> .0. = i )
11 eleq1 
 |-  ( i = .0. -> ( i e. B <-> .0. e. B ) )
12 oveq1 
 |-  ( i = .0. -> ( i .+ x ) = ( .0. .+ x ) )
13 12 eqeq1d 
 |-  ( i = .0. -> ( ( i .+ x ) = x <-> ( .0. .+ x ) = x ) )
14 13 ovanraleqv 
 |-  ( i = .0. -> ( A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) <-> A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
15 11 14 anbi12d 
 |-  ( i = .0. -> ( ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) <-> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
16 15 eqcoms 
 |-  ( .0. = i -> ( ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) <-> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
17 16 adantl 
 |-  ( ( ph /\ .0. = i ) -> ( ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) <-> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
18 17 biimpd 
 |-  ( ( ph /\ .0. = i ) -> ( ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
19 18 impancom 
 |-  ( ( ph /\ ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) ) -> ( .0. = i -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
20 10 19 mpd 
 |-  ( ( ph /\ ( i e. B /\ A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) ) ) -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )
21 20 rexlimdvaa 
 |-  ( ph -> ( E. i e. B A. x e. B ( ( i .+ x ) = x /\ ( x .+ i ) = x ) -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
22 8 21 biimtrid 
 |-  ( ph -> ( E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) ) )
23 4 22 mpd 
 |-  ( ph -> ( .0. e. B /\ A. x e. B ( ( .0. .+ x ) = x /\ ( x .+ .0. ) = x ) ) )