Description: Obsolete version of mndideu as of 18-Aug-2026. The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of Herstein p. 55. (Contributed by Mario Carneiro, 8-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mndcl.b | |- B = ( Base ` G ) |
|
| mndcl.p | |- .+ = ( +g ` G ) |
||
| Assertion | mndideuOLD | |- ( 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 | mndid | |- ( G e. Mnd -> E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |
| 4 | mgmidmo | |- E* u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) |
|
| 5 | reu5 | |- ( E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) <-> ( E. u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) /\ E* u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) ) |
|
| 6 | 3 4 5 | sylanblrc | |- ( G e. Mnd -> E! u e. B A. x e. B ( ( u .+ x ) = x /\ ( x .+ u ) = x ) ) |