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 )