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
|- .x. = ( .r ` R )
ringz.z
|- .0. = ( 0g ` R )
Assertion ringlz
|- ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .0. )

Proof

Step Hyp Ref Expression
1 ringz.b
 |-  B = ( Base ` R )
2 ringz.t
 |-  .x. = ( .r ` R )
3 ringz.z
 |-  .0. = ( 0g ` R )
4 ringrng
 |-  ( R e. Ring -> R e. Rng )
5 1 2 3 rnglz
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = .0. )
6 4 5 sylan
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .0. )