Theorem mndideu

Description: 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)

	Ref	Expression
Hypotheses	mndcl.b	$$⊢B={\mathrm{Base}}_G$$
	mndcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	mndideu	$$⊢G\in \mathrm{Mnd}\to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	$$⊢B={\mathrm{Base}}_G$$
2		mndcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	mndid	$$⊢G\in \mathrm{Mnd}\to \exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
4		mgmidmo	$$⊢{\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$
5		reu5	$$⊢\exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\leftrightarrow \left(\exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\wedge {\exists }^{*}u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\right)$$
6	3 4 5	sylanblrc	$$⊢G\in \mathrm{Mnd}\to \exists !u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)$$