# Metamath Proof Explorer

## Theorem ringrz

Description: The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009)

Ref Expression
Hypotheses rngz.b
`|- B = ( Base ` R )`
rngz.t
`|- .x. = ( .r ` R )`
rngz.z
`|- .0. = ( 0g ` R )`
Assertion ringrz
`|- ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )`

### Proof

Step Hyp Ref Expression
1 rngz.b
` |-  B = ( Base ` R )`
2 rngz.t
` |-  .x. = ( .r ` R )`
3 rngz.z
` |-  .0. = ( 0g ` R )`
4 ringgrp
` |-  ( R e. Ring -> R e. Grp )`
5 1 3 grpidcl
` |-  ( R e. Grp -> .0. e. B )`
6 eqid
` |-  ( +g ` R ) = ( +g ` R )`
7 1 6 3 grplid
` |-  ( ( R e. Grp /\ .0. e. B ) -> ( .0. ( +g ` R ) .0. ) = .0. )`
8 4 5 7 syl2anc2
` |-  ( R e. Ring -> ( .0. ( +g ` R ) .0. ) = .0. )`
` |-  ( ( R e. Ring /\ X e. B ) -> ( .0. ( +g ` R ) .0. ) = .0. )`
10 9 oveq2d
` |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. ( .0. ( +g ` R ) .0. ) ) = ( X .x. .0. ) )`
11 simpr
` |-  ( ( R e. Ring /\ X e. B ) -> X e. B )`
12 4 5 syl
` |-  ( R e. Ring -> .0. e. B )`
` |-  ( ( R e. Ring /\ X e. B ) -> .0. e. B )`
14 11 13 13 3jca
` |-  ( ( R e. Ring /\ X e. B ) -> ( X e. B /\ .0. e. B /\ .0. e. B ) )`
15 1 6 2 ringdi
` |-  ( ( R e. Ring /\ ( X e. B /\ .0. e. B /\ .0. e. B ) ) -> ( X .x. ( .0. ( +g ` R ) .0. ) ) = ( ( X .x. .0. ) ( +g ` R ) ( X .x. .0. ) ) )`
16 14 15 syldan
` |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. ( .0. ( +g ` R ) .0. ) ) = ( ( X .x. .0. ) ( +g ` R ) ( X .x. .0. ) ) )`
` |-  ( ( R e. Ring /\ X e. B ) -> R e. Grp )`
18 1 2 ringcl
` |-  ( ( R e. Ring /\ X e. B /\ .0. e. B ) -> ( X .x. .0. ) e. B )`
19 13 18 mpd3an3
` |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) e. B )`
20 1 6 3 grplid
` |-  ( ( R e. Grp /\ ( X .x. .0. ) e. B ) -> ( .0. ( +g ` R ) ( X .x. .0. ) ) = ( X .x. .0. ) )`
21 20 eqcomd
` |-  ( ( R e. Grp /\ ( X .x. .0. ) e. B ) -> ( X .x. .0. ) = ( .0. ( +g ` R ) ( X .x. .0. ) ) )`
22 17 19 21 syl2anc
` |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = ( .0. ( +g ` R ) ( X .x. .0. ) ) )`
23 10 16 22 3eqtr3d
` |-  ( ( R e. Ring /\ X e. B ) -> ( ( X .x. .0. ) ( +g ` R ) ( X .x. .0. ) ) = ( .0. ( +g ` R ) ( X .x. .0. ) ) )`
24 1 6 grprcan
` |-  ( ( R e. Grp /\ ( ( X .x. .0. ) e. B /\ .0. e. B /\ ( X .x. .0. ) e. B ) ) -> ( ( ( X .x. .0. ) ( +g ` R ) ( X .x. .0. ) ) = ( .0. ( +g ` R ) ( X .x. .0. ) ) <-> ( X .x. .0. ) = .0. ) )`
25 17 19 13 19 24 syl13anc
` |-  ( ( R e. Ring /\ X e. B ) -> ( ( ( X .x. .0. ) ( +g ` R ) ( X .x. .0. ) ) = ( .0. ( +g ` R ) ( X .x. .0. ) ) <-> ( X .x. .0. ) = .0. ) )`
26 23 25 mpbid
` |-  ( ( R e. Ring /\ X e. B ) -> ( X .x. .0. ) = .0. )`