Metamath Proof Explorer

Theorem rngorz

Description: The zero of a unital ring is a right-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 rngorz 
|- ( ( R e. RingOps /\ A e. X ) -> ( A H Z ) = 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 oveq2d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( Z G Z ) ) = ( A H Z ) )
11 simpr 
 |-  ( ( R e. RingOps /\ A e. X ) -> A e. X )
12 3 2 1 rngo0cl 
 |-  ( R e. RingOps -> Z e. X )
13 12 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> Z e. X )
14 11 13 13 3jca 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A e. X /\ Z e. X /\ Z e. X ) )
15 3 4 2 rngodi 
 |-  ( ( R e. RingOps /\ ( A e. X /\ Z e. X /\ Z e. X ) ) -> ( A H ( Z G Z ) ) = ( ( A H Z ) G ( A H Z ) ) )
16 14 15 syldan 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H ( Z G Z ) ) = ( ( A H Z ) G ( A H Z ) ) )
17 5 adantr 
 |-  ( ( R e. RingOps /\ A e. X ) -> G e. GrpOp )
18 3 4 2 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ Z e. X ) -> ( A H Z ) e. X )
19 13 18 mpd3an3 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H Z ) e. X )
20 2 1 grpolid 
 |-  ( ( G e. GrpOp /\ ( A H Z ) e. X ) -> ( Z G ( A H Z ) ) = ( A H Z ) )
21 20 eqcomd 
 |-  ( ( G e. GrpOp /\ ( A H Z ) e. X ) -> ( A H Z ) = ( Z G ( A H Z ) ) )
22 17 19 21 syl2anc 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H Z ) = ( Z G ( A H Z ) ) )
23 10 16 22 3eqtr3d 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( A H Z ) G ( A H Z ) ) = ( Z G ( A H Z ) ) )
24 2 grporcan 
 |-  ( ( G e. GrpOp /\ ( ( A H Z ) e. X /\ Z e. X /\ ( A H Z ) e. X ) ) -> ( ( ( A H Z ) G ( A H Z ) ) = ( Z G ( A H Z ) ) <-> ( A H Z ) = Z ) )
25 17 19 13 19 24 syl13anc 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( ( ( A H Z ) G ( A H Z ) ) = ( Z G ( A H Z ) ) <-> ( A H Z ) = Z ) )
26 23 25 mpbid 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( A H Z ) = Z )