This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ismgmid2

Description: Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses ismgmid.b 
|- B = ( Base ` G )
ismgmid.o 
|- .0. = ( 0g ` G )
ismgmid.p 
|- .+ = ( +g ` G )
ismgmid2.u 
|- ( ph -> U e. B )
ismgmid2.l 
|- ( ( ph /\ x e. B ) -> ( U .+ x ) = x )
ismgmid2.r 
|- ( ( ph /\ x e. B ) -> ( x .+ U ) = x )
Assertion ismgmid2 
|- ( ph -> U = .0. )

Proof

Step Hyp Ref Expression
1 ismgmid.b 
 |-  B = ( Base ` G )
2 ismgmid.o 
 |-  .0. = ( 0g ` G )
3 ismgmid.p 
 |-  .+ = ( +g ` G )
4 ismgmid2.u 
 |-  ( ph -> U e. B )
5 ismgmid2.l 
 |-  ( ( ph /\ x e. B ) -> ( U .+ x ) = x )
6 ismgmid2.r 
 |-  ( ( ph /\ x e. B ) -> ( x .+ U ) = x )
7 5 6 jca 
 |-  ( ( ph /\ x e. B ) -> ( ( U .+ x ) = x /\ ( x .+ U ) = x ) )
8 7 ralrimiva 
 |-  ( ph -> A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = 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 rspcev 
 |-  ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
13 4 8 12 syl2anc 
 |-  ( ph -> E. e e. B A. x e. B ( ( e .+ x ) = x /\ ( x .+ e ) = x ) )
14 1 2 3 13 ismgmid 
 |-  ( ph -> ( ( U e. B /\ A. x e. B ( ( U .+ x ) = x /\ ( x .+ U ) = x ) ) <-> .0. = U ) )
15 4 8 14 mpbi2and 
 |-  ( ph -> .0. = U )
16 15 eqcomd 
 |-  ( ph -> U = .0. )