Metamath Proof Explorer


Theorem ringridm

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

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

Proof

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