Metamath Proof Explorer


Theorem ringridmd

Description: The unity element of a ring is a right multiplicative identity. (Contributed by SN, 14-Aug-2024)

Ref Expression
Hypotheses ringlidmd.b B = Base R
ringlidmd.t · ˙ = R
ringlidmd.u 1 ˙ = 1 R
ringlidmd.r φ R Ring
ringlidmd.x φ X B
Assertion ringridmd φ X · ˙ 1 ˙ = X

Proof

Step Hyp Ref Expression
1 ringlidmd.b B = Base R
2 ringlidmd.t · ˙ = R
3 ringlidmd.u 1 ˙ = 1 R
4 ringlidmd.r φ R Ring
5 ringlidmd.x φ X B
6 1 2 3 ringridm R Ring X B X · ˙ 1 ˙ = X
7 4 5 6 syl2anc φ X · ˙ 1 ˙ = X