mndid

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

	Ref	Expression
Hypotheses	mndcl.b	$⊢ B = {Base}_{G}$
	mndcl.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mndid	$⊢ G \in Mnd \to \exists u \in B \forall x \in B (u \underset{˙}{+} x = x \land x \underset{˙}{+} u = x)$

Step	Hyp	Ref	Expression
1		mndcl.b	$⊢ B = {Base}_{G}$
2		mndcl.p	$⊢ \underset{˙}{+} = +_{G}$
3	1 2	ismnd	$⊢ G \in Mnd \leftrightarrow (\forall x \in B \forall y \in B (x \underset{˙}{+} y \in B \land \forall z \in B (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)) \land \exists u \in B \forall x \in B (u \underset{˙}{+} x = x \land x \underset{˙}{+} u = x))$
4	3	simprbi	$⊢ G \in Mnd \to \exists u \in B \forall x \in B (u \underset{˙}{+} x = x \land x \underset{˙}{+} u = x)$

Metamath Proof Explorer