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 RngHomo 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 RngHomo 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 RngHomo R ) )