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

Metamath Proof Explorer

Theorem mgmidsssn0

Description: Property of the set of identities of G . Either G has no identities, and O = (/) , or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014)

Ref Expression
Hypotheses mgmidsssn0.b 
|- B = ( Base ` G )
mgmidsssn0.z 
|- .0. = ( 0g ` G )
mgmidsssn0.p 
|- .+ = ( +g ` G )
mgmidsssn0.o 
|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
Assertion mgmidsssn0 
|- ( G e. V -> O C_ { .0. } )

Proof

Step Hyp Ref Expression
1 mgmidsssn0.b 
 |-  B = ( Base ` G )
2 mgmidsssn0.z 
 |-  .0. = ( 0g ` G )
3 mgmidsssn0.p 
 |-  .+ = ( +g ` G )
4 mgmidsssn0.o 
 |-  O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
5 simpr 
 |-  ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
6 oveq1 
 |-  ( z = x -> ( z .+ y ) = ( x .+ y ) )
7 6 eqeq1d 
 |-  ( z = x -> ( ( z .+ y ) = y <-> ( x .+ y ) = y ) )
8 7 ovanraleqv 
 |-  ( z = x -> ( A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
9 8 rspcev 
 |-  ( ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) -> E. z e. B A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) )
10 9 adantl 
 |-  ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> E. z e. B A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) )
11 1 2 3 10 ismgmid 
 |-  ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> ( ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) <-> .0. = x ) )
12 5 11 mpbid 
 |-  ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> .0. = x )
13 12 eqcomd 
 |-  ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> x = .0. )
14 velsn 
 |-  ( x e. { .0. } <-> x = .0. )
15 13 14 sylibr 
 |-  ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> x e. { .0. } )
16 15 expr 
 |-  ( ( G e. V /\ x e. B ) -> ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) )
17 16 ralrimiva 
 |-  ( G e. V -> A. x e. B ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) )
18 rabss 
 |-  ( { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { .0. } <-> A. x e. B ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) )
19 17 18 sylibr 
 |-  ( G e. V -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { .0. } )
20 4 19 eqsstrid 
 |-  ( G e. V -> O C_ { .0. } )