Metamath Proof Explorer

Theorem rnglz

Description: The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009) Generalization of ringlz . (Revised by AV, 17-Apr-2020)

Ref Expression
Hypotheses rngcl.b 
|- B = ( Base ` R )
rngcl.t 
|- .x. = ( .r ` R )
rnglz.z 
|- .0. = ( 0g ` R )
Assertion rnglz 
|- ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = .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 rngabl 
 |-  ( R e. Rng -> R e. Abel )
5 ablgrp 
 |-  ( R e. Abel -> R e. Grp )
6 4 5 syl 
 |-  ( R e. Rng -> R e. Grp )
7 1 3 grpidcl 
 |-  ( R e. Grp -> .0. e. B )
8 eqid 
 |-  ( +g ` R ) = ( +g ` R )
9 1 8 3 grplid 
 |-  ( ( R e. Grp /\ .0. e. B ) -> ( .0. ( +g ` R ) .0. ) = .0. )
10 6 7 9 syl2anc2 
 |-  ( R e. Rng -> ( .0. ( +g ` R ) .0. ) = .0. )
11 10 adantr 
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. ( +g ` R ) .0. ) = .0. )
12 11 oveq1d 
 |-  ( ( R e. Rng /\ X e. B ) -> ( ( .0. ( +g ` R ) .0. ) .x. X ) = ( .0. .x. X ) )
13 simpl 
 |-  ( ( R e. Rng /\ X e. B ) -> R e. Rng )
14 6 7 syl 
 |-  ( R e. Rng -> .0. e. B )
15 14 14 jca 
 |-  ( R e. Rng -> ( .0. e. B /\ .0. e. B ) )
16 15 anim1i 
 |-  ( ( R e. Rng /\ X e. B ) -> ( ( .0. e. B /\ .0. e. B ) /\ X e. B ) )
17 df-3an 
 |-  ( ( .0. e. B /\ .0. e. B /\ X e. B ) <-> ( ( .0. e. B /\ .0. e. B ) /\ X e. B ) )
18 16 17 sylibr 
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. e. B /\ .0. e. B /\ X e. B ) )
19 1 8 2 rngdir 
 |-  ( ( R e. Rng /\ ( .0. e. B /\ .0. e. B /\ X e. B ) ) -> ( ( .0. ( +g ` R ) .0. ) .x. X ) = ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) )
20 13 18 19 syl2anc 
 |-  ( ( R e. Rng /\ X e. B ) -> ( ( .0. ( +g ` R ) .0. ) .x. X ) = ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) )
21 6 adantr 
 |-  ( ( R e. Rng /\ X e. B ) -> R e. Grp )
22 14 adantr 
 |-  ( ( R e. Rng /\ X e. B ) -> .0. e. B )
23 simpr 
 |-  ( ( R e. Rng /\ X e. B ) -> X e. B )
24 1 2 rngcl 
 |-  ( ( R e. Rng /\ .0. e. B /\ X e. B ) -> ( .0. .x. X ) e. B )
25 13 22 23 24 syl3anc 
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) e. B )
26 1 8 3 grprid 
 |-  ( ( R e. Grp /\ ( .0. .x. X ) e. B ) -> ( ( .0. .x. X ) ( +g ` R ) .0. ) = ( .0. .x. X ) )
27 26 eqcomd 
 |-  ( ( R e. Grp /\ ( .0. .x. X ) e. B ) -> ( .0. .x. X ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) )
28 21 25 27 syl2anc 
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) )
29 12 20 28 3eqtr3d 
 |-  ( ( R e. Rng /\ X e. B ) -> ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) )
30 1 8 grplcan 
 |-  ( ( R e. Grp /\ ( ( .0. .x. X ) e. B /\ .0. e. B /\ ( .0. .x. X ) e. B ) ) -> ( ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) <-> ( .0. .x. X ) = .0. ) )
31 21 25 22 25 30 syl13anc 
 |-  ( ( R e. Rng /\ X e. B ) -> ( ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) <-> ( .0. .x. X ) = .0. ) )
32 29 31 mpbid 
 |-  ( ( R e. Rng /\ X e. B ) -> ( .0. .x. X ) = .0. )