Metamath Proof Explorer


Theorem ringlidm

Description: The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011)

Ref Expression
Hypotheses ringidm.b B=BaseR
ringidm.t ·˙=R
ringidm.u 1˙=1R
Assertion ringlidm RRingXB1˙·˙X=X

Proof

Step Hyp Ref Expression
1 ringidm.b B=BaseR
2 ringidm.t ·˙=R
3 ringidm.u 1˙=1R
4 1 2 3 ringidmlem RRingXB1˙·˙X=XX·˙1˙=X
5 4 simpld RRingXB1˙·˙X=X