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
|- .x. = ( .r ` R )
ringz.z
|- .0. = ( 0g ` R )
Assertion ringrz
|- ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .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 rngrz
 |-  ( ( R e. Rng /\ X e. B ) -> ( X .x. .0. ) = .0. )
6 4 5 sylan
 |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )