This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngrz

Description: The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009) Generalization of ringrz . (Revised by AV, 16-Feb-2025)

Ref Expression
Hypotheses rngcl.b 
|- B = ( Base ` R )
rngcl.t 
|- .x. = ( .r ` R )
rnglz.z 
|- .0. = ( 0g ` R )
Assertion rngrz 
|- ( ( R e. Rng /\ X e. B ) -> ( X .x. .0. ) = .0. )

Proof

Step Hyp Ref Expression
1 rngcl.b 
 |-  B = ( Base ` R )
2 rngcl.t 
 |-  .x. = ( .r ` R )
3 rnglz.z 
 |-  .0. = ( 0g ` R )
4 rnggrp 
 |-  ( R e. Rng -> 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. Rng -> ( .0. ( +g ` R ) .0. ) = .0. )
9 8 adantr 
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. ( +g ` R ) .0. ) = .0. )
10 9 oveq2d 
 |-  ( ( R e. Rng /\ X e. B ) -> ( X .x. ( .0. ( +g ` R ) .0. ) ) = ( X .x. .0. ) )
11 simpr 
 |-  ( ( R e. Rng /\ X e. B ) -> X e. B )
12 1 3 rng0cl 
 |-  ( R e. Rng -> .0. e. B )
13 12 adantr 
 |-  ( ( R e. Rng /\ X e. B ) -> .0. e. B )
14 11 13 13 3jca 
 |-  ( ( R e. Rng /\ X e. B ) -> ( X e. B /\ .0. e. B /\ .0. e. B ) )
15 1 6 2 rngdi 
 |-  ( ( R e. Rng /\ ( 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. Rng /\ X e. B ) -> ( X .x. ( .0. ( +g ` R ) .0. ) ) = ( ( X .x. .0. ) ( +g ` R ) ( X .x. .0. ) ) )
17 4 adantr 
 |-  ( ( R e. Rng /\ X e. B ) -> R e. Grp )
18 1 2 rngcl 
 |-  ( ( R e. Rng /\ X e. B /\ .0. e. B ) -> ( X .x. .0. ) e. B )
19 13 18 mpd3an3 
 |-  ( ( R e. Rng /\ 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. Rng /\ X e. B ) -> ( X .x. .0. ) = ( .0. ( +g ` R ) ( X .x. .0. ) ) )
23 10 16 22 3eqtr3d 
 |-  ( ( R e. Rng /\ 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. Rng /\ 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. Rng /\ X e. B ) -> ( X .x. .0. ) = .0. )