Theorem lmhmf

Description: A homomorphism of left modules is a function. (Contributed by Stefan O'Rear, 1-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lmhmf.b	$$⊢B={\mathrm{Base}}_S$$
2		lmhmf.c	$$⊢C={\mathrm{Base}}_T$$
3		lmghm	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to F\in \left(S\mathrm{GrpHom}T\right)$$
4	1 2	ghmf	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F:B⟶C$$
5	3 4	syl	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to F:B⟶C$$