Metamath Proof Explorer


Theorem ringlz

Description: The zero of a unital ring is a left-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 ringlz ( ( 𝑅 ∈ 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 rnglz ( ( 𝑅 ∈ Rng ∧ 𝑋𝐵 ) → ( 0 · 𝑋 ) = 0 )
6 4 5 sylan ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵 ) → ( 0 · 𝑋 ) = 0 )