Theorem mndid

Description: A monoid has a two-sided identity element. (Contributed by FL, 2-Nov-2009) (Revised by NM, 16-Aug-2011)

	Ref	Expression
Hypotheses	mndcl.b	$$⊢B={\mathrm{Base}}_G$$
	mndcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		mndcl.b	$$⊢B={\mathrm{Base}}_G$$
2		mndcl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3	1 2	ismnd	$$⊢G\in \mathrm{Mnd}\leftrightarrow \left(\forall x\in B\forall y\in B\left(x\underset{\dot{}}{+}y\in B\wedge \forall z\in B\left(x\underset{\dot{}}{+}y\right)\underset{\dot{}}{+}z=x\underset{\dot{}}{+}\left(y\underset{\dot{}}{+}z\right)\right)\wedge \exists u\in B\forall x\in B\left(u\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}u=x\right)\right)$$
4	3	simprbi	$$⊢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)$$