rnghmghm

Description: A non-unital ring homomorphism is an additive group homomorphism. (Contributed by AV, 23-Feb-2020)

		Ref	Expression
	Assertion	rnghmghm	$⊢ F \in (R RngHomo S) \to F \in (R GrpHom S)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ \cdot_{R} = \cdot_{R}$
3		eqid	$⊢ \cdot_{S} = \cdot_{S}$
4	1 2 3	isrnghm	$⊢ F \in (R RngHomo S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y)))$
5		simprl	$⊢ ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x \cdot_{R} y) = F (x) \cdot_{S} F (y))) \to F \in (R GrpHom S)$
6	4 5	sylbi	$⊢ F \in (R RngHomo S) \to F \in (R GrpHom S)$

Metamath Proof Explorer