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={\mathrm{mulGrp}}_R$$
	isrnghmmul.n	$$⊢N={\mathrm{mulGrp}}_S$$
Assertion	rnghmmgmhm	$$⊢F\in \left(R\mathrm{RngHom}S\right)\to F\in \left(M\mathrm{MgmHom}N\right)$$

Proof

Step	Hyp	Ref	Expression
1		isrnghmmul.m	$$⊢M={\mathrm{mulGrp}}_R$$
2		isrnghmmul.n	$$⊢N={\mathrm{mulGrp}}_S$$
3	1 2	isrnghmmul	$$⊢F\in \left(R\mathrm{RngHom}S\right)\leftrightarrow \left(\left(R\in \mathrm{Rng}\wedge S\in \mathrm{Rng}\right)\wedge \left(F\in \left(R\mathrm{GrpHom}S\right)\wedge F\in \left(M\mathrm{MgmHom}N\right)\right)\right)$$
4	3	simprbi	$$⊢F\in \left(R\mathrm{RngHom}S\right)\to \left(F\in \left(R\mathrm{GrpHom}S\right)\wedge F\in \left(M\mathrm{MgmHom}N\right)\right)$$
5	4	simprd	$$⊢F\in \left(R\mathrm{RngHom}S\right)\to F\in \left(M\mathrm{MgmHom}N\right)$$