Metamath Proof Explorer

Theorem ismgmid

Description: The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014)

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 ismgmid 
|- ( ph -> ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) <-> .0. = U ) )

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 id 
 |-  ( U e. B -> U e. B )
6 mgmidmo 
 |-  E* e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x )
7 reu5 
 |-  ( E! e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> ( E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) /\ E* e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
8 4 6 7 sylanblrc 
 |-  ( ph -> E! e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
9 oveq1 
 |-  ( e = U -> ( e .+ x ) = ( U .+ x ) )
10 9 eqeq1d 
 |-  ( e = U -> ( ( e .+ x ) = x <-> ( U .+ x ) = x ) )
11 10 ovanraleqv 
 |-  ( e = U -> ( A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) <-> A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) )
12 11 riota2 
 |-  ( ( U e. B /\ E! e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) -> ( A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) <-> ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U ) )
13 5 8 12 syl2anr 
 |-  ( ( ph /\ U e. B ) -> ( A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) <-> ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U ) )
14 13 pm5.32da 
 |-  ( ph -> ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) <-> ( U e. B /\ ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U ) ) )
15 riotacl 
 |-  ( E! e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) -> ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) e. B )
16 8 15 syl 
 |-  ( ph -> ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) e. B )
17 eleq1 
 |-  ( ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U -> ( ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) e. B <-> U e. B ) )
18 16 17 syl5ibcom 
 |-  ( ph -> ( ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U -> U e. B ) )
19 18 pm4.71rd 
 |-  ( ph -> ( ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U <-> ( U e. B /\ ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U ) ) )
20 df-riota 
 |-  ( iota_ 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 ) ) )
21 1 3 2 grpidval 
 |-  .0. = ( iota e ( e e. B /\ A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) )
22 20 21 eqtr4i 
 |-  ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = .0.
23 22 eqeq1i 
 |-  ( ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U <-> .0. = U )
24 23 a1i 
 |-  ( ph -> ( ( iota_ e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) ) = U <-> .0. = U ) )
25 14 19 24 3bitr2d 
 |-  ( ph -> ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) <-> .0. = U ) )