rhmghm

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

		Ref	Expression
	Assertion	rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$

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

Metamath Proof Explorer