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=BaseG
mndlrid.p +˙=+G
mndlrid.o 0˙=0G
Assertion mndrid GMndXBX+˙0˙=X

Proof

Step Hyp Ref Expression
1 mndlrid.b B=BaseG
2 mndlrid.p +˙=+G
3 mndlrid.o 0˙=0G
4 1 2 3 mndlrid GMndXB0˙+˙X=XX+˙0˙=X
5 4 simprd GMndXBX+˙0˙=X