Metamath Proof Explorer

Theorem rhmisrnghm

Description: Each unital ring homomorphism is a non-unital ring homomorphism. (Contributed by AV, 29-Feb-2020)

Ref Expression
Assertion rhmisrnghm 
|- ( F e. ( R RingHom S ) -> F e. ( R RngHomo S ) )

Proof

Step Hyp Ref Expression
1 ringrng 
 |-  ( R e. Ring -> R e. Rng )
2 ringrng 
 |-  ( S e. Ring -> S e. Rng )
3 1 2 anim12i 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( R e. Rng /\ S e. Rng ) )
4 mhmismgmhm 
 |-  ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) -> F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) )
5 4 anim2i 
 |-  ( ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) -> ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) )
6 3 5 anim12i 
 |-  ( ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) -> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) )
7 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
8 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
9 7 8 isrhm 
 |-  ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) )
10 7 8 isrnghmmul 
 |-  ( F e. ( R RngHomo S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MgmHom ( mulGrp ` S ) ) ) ) )
11 6 9 10 3imtr4i 
 |-  ( F e. ( R RingHom S ) -> F e. ( R RngHomo S ) )