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	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	isrhm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑆 )
Assertion	rhmmhm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		isrhm.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		isrhm.n	⊢ 𝑁 = ( mulGrp ‘ 𝑆 )
3	1 2	isrhm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) ) )
4	3	simprbi	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) )
5	4	simprd	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )