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 B = Base R
ringz.t · ˙ = R
ringz.z 0 ˙ = 0 R
Assertion ringrz R Ring X B X · ˙ 0 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 ringz.b B = Base R
2 ringz.t · ˙ = R
3 ringz.z 0 ˙ = 0 R
4 ringrng R Ring R Rng
5 1 2 3 rngrz R Rng X B X · ˙ 0 ˙ = 0 ˙
6 4 5 sylan R Ring X B X · ˙ 0 ˙ = 0 ˙