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 𝐵 = ( Base ‘ 𝑅 )
ringlidmd.t · = ( .r𝑅 )
ringlidmd.u 1 = ( 1r𝑅 )
ringlidmd.r ( 𝜑𝑅 ∈ Ring )
ringlidmd.x ( 𝜑𝑋𝐵 )
Assertion ringridmd ( 𝜑 → ( 𝑋 · 1 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ringlidmd.b 𝐵 = ( Base ‘ 𝑅 )
2 ringlidmd.t · = ( .r𝑅 )
3 ringlidmd.u 1 = ( 1r𝑅 )
4 ringlidmd.r ( 𝜑𝑅 ∈ Ring )
5 ringlidmd.x ( 𝜑𝑋𝐵 )
6 1 2 3 ringridm ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 𝑋 · 1 ) = 𝑋 )
7 4 5 6 syl2anc ( 𝜑 → ( 𝑋 · 1 ) = 𝑋 )