Metamath Proof Explorer


Theorem ringlidm

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

Ref Expression
Hypotheses rngidm.b B = Base R
rngidm.t · ˙ = R
rngidm.u 1 ˙ = 1 R
Assertion ringlidm R Ring X B 1 ˙ · ˙ X = X

Proof

Step Hyp Ref Expression
1 rngidm.b B = Base R
2 rngidm.t · ˙ = R
3 rngidm.u 1 ˙ = 1 R
4 1 2 3 ringidmlem R Ring X B 1 ˙ · ˙ X = X X · ˙ 1 ˙ = X
5 4 simpld R Ring X B 1 ˙ · ˙ X = X