Metamath Proof Explorer

Theorem rhmghm

Description: A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion rhmghm 
|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
2 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
3 1 2 isrhm 
 |-  ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) )
4 3 simprbi 
 |-  ( F e. ( R RingHom S ) -> ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
5 4 simpld 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )