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 e. ( R RingHom S ) -> F e. ( M MndHom N ) )

Proof

Step	Hyp	Ref	Expression
1		isrhm.m	|- M = ( mulGrp ` R )
2		isrhm.n	|- N = ( mulGrp ` S )
3	1 2	isrhm	|- ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) ) )
4	3	simprbi	|- ( F e. ( R RingHom S ) -> ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) )
5	4	simprd	|- ( F e. ( R RingHom S ) -> F e. ( M MndHom N ) )