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. } )