Description: The two-sided identity element of a group is unique. Lemma 2.2.1(a) of Herstein p. 55. (Contributed by NM, 16-Aug-2011) (Revised by Mario Carneiro, 8-Dec-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | grpcl.b | |- B = ( Base ` G ) |
|
| grpcl.p | |- .+ = ( +g ` G ) |
||
| grpinvex.p | |- .0. = ( 0g ` G ) |
||
| Assertion | grpideu | |- ( G e. Grp -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpcl.b | |- B = ( Base ` G ) |
|
| 2 | grpcl.p | |- .+ = ( +g ` G ) |
|
| 3 | grpinvex.p | |- .0. = ( 0g ` G ) |
|
| 4 | grpmnd | |- ( G e. Grp -> G e. Mnd ) |
|
| 5 | 1 2 | mndideu | |- ( G e. Mnd -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |
| 6 | 4 5 | syl | |- ( G e. Grp -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |