Metamath Proof Explorer

Theorem rnghmmgmhm

Description: A non-unital ring homomorphism is a homomorphism of multiplicative magmas. (Contributed by AV, 27-Feb-2020)

	Ref	Expression
Hypotheses	isrnghmmul.m	$⊢ M = {mulGrp}_{R}$
	isrnghmmul.n	$⊢ N = {mulGrp}_{S}$
Assertion	rnghmmgmhm	$⊢ F \in (R RngHomo S) \to F \in (M MgmHom N)$

Step	Hyp	Ref	Expression
1		isrnghmmul.m	$⊢ M = {mulGrp}_{R}$
2		isrnghmmul.n	$⊢ N = {mulGrp}_{S}$
3	1 2	isrnghmmul	$⊢ F \in (R RngHomo S) \leftrightarrow ((R \in Rng \land S \in Rng) \land (F \in (R GrpHom S) \land F \in (M MgmHom N)))$
4	3	simprbi	$⊢ F \in (R RngHomo S) \to (F \in (R GrpHom S) \land F \in (M MgmHom N))$
5	4	simprd	$⊢ F \in (R RngHomo S) \to F \in (M MgmHom N)$