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	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	isrnghmmul.n	⊢ 𝑁 = ( mulGrp ‘ 𝑆 )
Assertion	rnghmmgmhm	⊢ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) → 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		isrnghmmul.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		isrnghmmul.n	⊢ 𝑁 = ( mulGrp ‘ 𝑆 )
3	1 2	isrnghmmul	⊢ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( ( 𝑅 ∈ Rng ∧ 𝑆 ∈ Rng ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) ) )
4	3	simprbi	⊢ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) ) )
5	4	simprd	⊢ ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) → 𝐹 ∈ ( 𝑀 MgmHom 𝑁 ) )