Metamath Proof Explorer

Theorem rngolz

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

Ref Expression
Hypotheses ringlz.1 
|- Z = ( GId ` G )
ringlz.2 
|- X = ran G
ringlz.3 
|- G = ( 1st ` R )
ringlz.4 
|- H = ( 2nd ` R )
Assertion rngolz 
|- ( ( R e. RingOps /\ A e. X ) -> ( Z H A ) = Z )

Proof

Step Hyp Ref Expression
1 ringlz.1 
 |-  Z = ( GId ` G )
2 ringlz.2 
 |-  X = ran G
3 ringlz.3 
 |-  G = ( 1st ` R )
4 ringlz.4 
 |-  H = ( 2nd ` R )
5 3 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
6 2 1 grpoidcl 
 |-  ( G e. GrpOp -> Z e. X )
7 2 1 grpolid 
 |-  ( ( G e. GrpOp /\ Z e. X ) -> ( Z G Z ) = Z )
8 5 6 7 syl2anc2 
 |-  ( R e. RingOps -> ( Z G Z ) = Z )
9 8 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( Z G Z ) = Z )
10 9 oveq1d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( Z G Z ) H A ) = ( Z H A ) )
11 3 2 1 rngo0cl 
 |-  ( R e. RingOps -> Z e. X )
12 11 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> Z e. X )
13 simpr 
 |-  ( ( R e. RingOps /\ A e. X ) -> A e. X )
14 12 12 13 3jca 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( Z e. X /\ Z e. X /\ A e. X ) )
15 3 4 2 rngodir 
 |-  ( ( R e. RingOps /\ ( Z e. X /\ Z e. X /\ A e. X ) ) -> ( ( Z G Z ) H A ) = ( ( Z H A ) G ( Z H A ) ) )
16 14 15 syldan 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( Z G Z ) H A ) = ( ( Z H A ) G ( Z H A ) ) )
17 5 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> G e. GrpOp )
18 simpl 
 |-  ( ( R e. RingOps /\ A e. X ) -> R e. RingOps )
19 3 4 2 rngocl 
 |-  ( ( R e. RingOps /\ Z e. X /\ A e. X ) -> ( Z H A ) e. X )
20 18 12 13 19 syl3anc 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( Z H A ) e. X )
21 2 1 grporid 
 |-  ( ( G e. GrpOp /\ ( Z H A ) e. X ) -> ( ( Z H A ) G Z ) = ( Z H A ) )
22 21 eqcomd 
 |-  ( ( G e. GrpOp /\ ( Z H A ) e. X ) -> ( Z H A ) = ( ( Z H A ) G Z ) )
23 17 20 22 syl2anc 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( Z H A ) = ( ( Z H A ) G Z ) )
24 10 16 23 3eqtr3d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( Z H A ) G ( Z H A ) ) = ( ( Z H A ) G Z ) )
25 2 grpolcan 
 |-  ( ( G e. GrpOp /\ ( ( Z H A ) e. X /\ Z e. X /\ ( Z H A ) e. X ) ) -> ( ( ( Z H A ) G ( Z H A ) ) = ( ( Z H A ) G Z ) <-> ( Z H A ) = Z ) )
26 17 20 12 20 25 syl13anc 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( ( Z H A ) G ( Z H A ) ) = ( ( Z H A ) G Z ) <-> ( Z H A ) = Z ) )
27 24 26 mpbid 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( Z H A ) = Z )