Description: A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mndcl.b | |- B = ( Base ` G ) |
|
mndcl.p | |- .+ = ( +g ` G ) |
||
Assertion | mndid | |- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mndcl.b | |- B = ( Base ` G ) |
|
2 | mndcl.p | |- .+ = ( +g ` G ) |
|
3 | 1 2 | ismnd | |- ( G e. Mnd <-> ( A. x e. B A. y e. B ( ( x .+ y ) e. B /\ A. z e. B ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) ) /\ E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) ) |
4 | 3 | simprbi | |- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |