This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mndrid

Description: The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011)

	Ref	Expression
Hypotheses	mndlrid.b	$⊢ B = {Base}_{G}$
	mndlrid.p	$⊢ \underset{˙}{+} = +_{G}$
	mndlrid.o	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	mndrid	$⊢ (G \in Mnd \land X \in B) \to X \underset{˙}{+} \underset{˙}{0} = X$

Step	Hyp	Ref	Expression
1		mndlrid.b	$⊢ B = {Base}_{G}$
2		mndlrid.p	$⊢ \underset{˙}{+} = +_{G}$
3		mndlrid.o	$⊢ \underset{˙}{0} = 0_{G}$
4	1 2 3	mndlrid	$⊢ (G \in Mnd \land X \in B) \to (\underset{˙}{0} \underset{˙}{+} X = X \land X \underset{˙}{+} \underset{˙}{0} = X)$
5	4	simprd	$⊢ (G \in Mnd \land X \in B) \to X \underset{˙}{+} \underset{˙}{0} = X$