Theorem mgmhmf

Description: A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		mgmhmf.b	$$⊢B={\mathrm{Base}}_S$$
2		mgmhmf.c	$$⊢C={\mathrm{Base}}_T$$
3		eqid	$$⊢{+}_S={+}_S$$
4		eqid	$$⊢{+}_T={+}_T$$
5	1 2 3 4	ismgmhm	$$⊢F\in \left(S\mathrm{MgmHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\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)\right)\right)$$
6		simprl	$$⊢\left(\left(S\in \mathrm{Mgm}\wedge T\in \mathrm{Mgm}\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)\right)\right)\to F:B⟶C$$
7	5 6	sylbi	$$⊢F\in \left(S\mathrm{MgmHom}T\right)\to F:B⟶C$$