Metamath Proof Explorer

Theorem idrnghm

Description: The identity homomorphism on a non-unital ring. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypothesis idrnghm.b 
|- B = ( Base ` R )
Assertion idrnghm 
|- ( R e. Rng -> ( _I |` B ) e. ( R RngHom R ) )

Proof

Step Hyp Ref Expression
1 idrnghm.b 
 |-  B = ( Base ` R )
2 id 
 |-  ( R e. Rng -> R e. Rng )
3 2 2 jca 
 |-  ( R e. Rng -> ( R e. Rng /\ R e. Rng ) )
4 rngabl 
 |-  ( R e. Rng -> R e. Abel )
5 ablgrp 
 |-  ( R e. Abel -> R e. Grp )
6 1 idghm 
 |-  ( R e. Grp -> ( _I |` B ) e. ( R GrpHom R ) )
7 4 5 6 3syl 
 |-  ( R e. Rng -> ( _I |` B ) e. ( R GrpHom R ) )
8 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
9 8 rngmgp 
 |-  ( R e. Rng -> ( mulGrp ` R ) e. Smgrp )
10 sgrpmgm 
 |-  ( ( mulGrp ` R ) e. Smgrp -> ( mulGrp ` R ) e. Mgm )
11 8 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
12 11 idmgmhm 
 |-  ( ( mulGrp ` R ) e. Mgm -> ( _I |` B ) e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` R ) ) )
13 9 10 12 3syl 
 |-  ( R e. Rng -> ( _I |` B ) e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` R ) ) )
14 7 13 jca 
 |-  ( R e. Rng -> ( ( _I |` B ) e. ( R GrpHom R ) /\ ( _I |` B ) e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` R ) ) ) )
15 8 8 isrnghmmul 
 |-  ( ( _I |` B ) e. ( R RngHom R ) <-> ( ( R e. Rng /\ R e. Rng ) /\ ( ( _I |` B ) e. ( R GrpHom R ) /\ ( _I |` B ) e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` R ) ) ) ) )
16 3 14 15 sylanbrc 
 |-  ( R e. Rng -> ( _I |` B ) e. ( R RngHom R ) )