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 B = Base R
ringz.t · ˙ = R
ringz.z 0 ˙ = 0 R
Assertion ringlz R Ring X B 0 ˙ · ˙ X = 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 rnglz R Rng X B 0 ˙ · ˙ X = 0 ˙
6 4 5 sylan R Ring X B 0 ˙ · ˙ X = 0 ˙