# 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}\in \left({R}\mathrm{RingHom}{S}\right)\to {F}\in \left({R}\mathrm{GrpHom}{S}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
2 eqid ${⊢}{\mathrm{mulGrp}}_{{S}}={\mathrm{mulGrp}}_{{S}}$
3 1 2 isrhm ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)\right)$
4 3 simprbi ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)\to \left({F}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {F}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)$
5 4 simpld ${⊢}{F}\in \left({R}\mathrm{RingHom}{S}\right)\to {F}\in \left({R}\mathrm{GrpHom}{S}\right)$