Metamath Proof Explorer

Theorem ringlz

Description: The zero of a unital ring is a left-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 ringlz 
|- ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .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. )
9 8 adantr 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. ( +g ` R ) .0. ) = .0. )
10 9 oveq1d 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( .0. ( +g ` R ) .0. ) .x. X ) = ( .0. .x. X ) )
11 4 5 syl 
 |-  ( R e. Ring -> .0. e. B )
12 11 adantr 
 |-  ( ( R e. Ring /\ X e. B ) -> .0. e. B )
13 simpr 
 |-  ( ( R e. Ring /\ X e. B ) -> X e. B )
14 12 12 13 3jca 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. e. B /\ .0. e. B /\ X e. B ) )
15 1 6 2 ringdir 
 |-  ( ( R e. Ring /\ ( .0. e. B /\ .0. e. B /\ X e. B ) ) -> ( ( .0. ( +g ` R ) .0. ) .x. X ) = ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) )
16 14 15 syldan 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( .0. ( +g ` R ) .0. ) .x. X ) = ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) )
17 4 adantr 
 |-  ( ( R e. Ring /\ X e. B ) -> R e. Grp )
18 simpl 
 |-  ( ( R e. Ring /\ X e. B ) -> R e. Ring )
19 1 2 ringcl 
 |-  ( ( R e. Ring /\ .0. e. B /\ X e. B ) -> ( .0. .x. X ) e. B )
20 18 12 13 19 syl3anc 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) e. B )
21 1 6 3 grprid 
 |-  ( ( R e. Grp /\ ( .0. .x. X ) e. B ) -> ( ( .0. .x. X ) ( +g ` R ) .0. ) = ( .0. .x. X ) )
22 21 eqcomd 
 |-  ( ( R e. Grp /\ ( .0. .x. X ) e. B ) -> ( .0. .x. X ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) )
23 17 20 22 syl2anc 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) )
24 10 16 23 3eqtr3d 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) )
25 1 6 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. ) )
26 17 20 12 20 25 syl13anc 
 |-  ( ( R e. Ring /\ X e. B ) -> ( ( ( .0. .x. X ) ( +g ` R ) ( .0. .x. X ) ) = ( ( .0. .x. X ) ( +g ` R ) .0. ) <-> ( .0. .x. X ) = .0. ) )
27 24 26 mpbid 
 |-  ( ( R e. Ring /\ X e. B ) -> ( .0. .x. X ) = .0. )