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. ) |
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. ) |