Metamath Proof Explorer


Theorem ringrz

Description: The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009) (Proof shortened by AV, 30-Mar-2025)

Ref Expression
Hypotheses ringz.b 𝐵 = ( Base ‘ 𝑅 )
ringz.t · = ( .r𝑅 )
ringz.z 0 = ( 0g𝑅 )
Assertion ringrz ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 𝑋 · 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 ringz.b 𝐵 = ( Base ‘ 𝑅 )
2 ringz.t · = ( .r𝑅 )
3 ringz.z 0 = ( 0g𝑅 )
4 ringrng ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
5 1 2 3 rngrz ( ( 𝑅 ∈ Rng ∧ 𝑋𝐵 ) → ( 𝑋 · 0 ) = 0 )
6 4 5 sylan ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 𝑋 · 0 ) = 0 )