Metamath Proof Explorer

Theorem idrhm

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

Ref Expression
Hypothesis idrhm.b 
|- B = ( Base ` R )
Assertion idrhm 
|- ( R e. Ring -> ( _I |` B ) e. ( R RingHom R ) )

Proof

Step Hyp Ref Expression
1 idrhm.b 
 |-  B = ( Base ` R )
2 id 
 |-  ( R e. Ring -> R e. Ring )
3 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
4 1 idghm 
 |-  ( R e. Grp -> ( _I |` B ) e. ( R GrpHom R ) )
5 3 4 syl 
 |-  ( R e. Ring -> ( _I |` B ) e. ( R GrpHom R ) )
6 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
7 6 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
8 6 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
9 8 idmhm 
 |-  ( ( mulGrp ` R ) e. Mnd -> ( _I |` B ) e. ( ( mulGrp ` R ) MndHom ( mulGrp ` R ) ) )
10 7 9 syl 
 |-  ( R e. Ring -> ( _I |` B ) e. ( ( mulGrp ` R ) MndHom ( mulGrp ` R ) ) )
11 5 10 jca 
 |-  ( R e. Ring -> ( ( _I |` B ) e. ( R GrpHom R ) /\ ( _I |` B ) e. ( ( mulGrp ` R ) MndHom ( mulGrp ` R ) ) ) )
12 6 6 isrhm 
 |-  ( ( _I |` B ) e. ( R RingHom R ) <-> ( ( R e. Ring /\ R e. Ring ) /\ ( ( _I |` B ) e. ( R GrpHom R ) /\ ( _I |` B ) e. ( ( mulGrp ` R ) MndHom ( mulGrp ` R ) ) ) ) )
13 2 2 11 12 syl21anbrc 
 |-  ( R e. Ring -> ( _I |` B ) e. ( R RingHom R ) )