Theorem mndlrid

Description: A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011)

	Ref	Expression
Hypotheses	mndlrid.b	$$⊢B={\mathrm{Base}}_G$$
	mndlrid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mndlrid.o	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	mndlrid	$$⊢\left(G\in \mathrm{Mnd}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}X=X\wedge X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		mndlrid.b	$$⊢B={\mathrm{Base}}_G$$
2		mndlrid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mndlrid.o	$$⊢\underset{\dot{}}{0}=0_G$$
4	1 2	mndid	$$⊢G\in \mathrm{Mnd}\to \exists y\in B\forall x\in B\left(y\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}y=x\right)$$
5	1 3 2 4	mgmlrid	$$⊢\left(G\in \mathrm{Mnd}\wedge X\in B\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{+}X=X\wedge X\underset{\dot{}}{+}\underset{\dot{}}{0}=X\right)$$