Theorem mhmf

Description: A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	mhmf.b	$$⊢B={\mathrm{Base}}_S$$
	mhmf.c	$$⊢C={\mathrm{Base}}_T$$
Assertion	mhmf	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to F:B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		mhmf.b	$$⊢B={\mathrm{Base}}_S$$
2		mhmf.c	$$⊢C={\mathrm{Base}}_T$$
3		eqid	$$⊢{+}_S={+}_S$$
4		eqid	$$⊢{+}_T={+}_T$$
5		eqid	$$⊢0_S=0_S$$
6		eqid	$$⊢0_T=0_T$$
7	1 2 3 4 5 6	ismhm	$$⊢F\in \left(S\mathrm{MndHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Mnd}\wedge T\in \mathrm{Mnd}\right)\wedge \left(F:B⟶C\wedge \forall x\in B\forall y\in BF\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)\wedge F\left(0_S\right)=0_T\right)\right)$$
8	7	simprbi	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to \left(F:B⟶C\wedge \forall x\in B\forall y\in BF\left(x{+}_{S}y\right)=F\left(x\right){+}_{T}F\left(y\right)\wedge F\left(0_S\right)=0_T\right)$$
9	8	simp1d	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to F:B⟶C$$