Metamath Proof Explorer

Theorem rhmmhm

Description: A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015)

	Ref	Expression
Hypotheses	isrhm.m	$⊢ M = {mulGrp}_{R}$
	isrhm.n	$⊢ N = {mulGrp}_{S}$
Assertion	rhmmhm	$⊢ F \in (R RingHom S) \to F \in (M MndHom N)$

Step	Hyp	Ref	Expression
1		isrhm.m	$⊢ M = {mulGrp}_{R}$
2		isrhm.n	$⊢ N = {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 (M MndHom N)))$
4	3	simprbi	$⊢ F \in (R RingHom S) \to (F \in (R GrpHom S) \land F \in (M MndHom N))$
5	4	simprd	$⊢ F \in (R RingHom S) \to F \in (M MndHom N)$