Theorem lmhmlmod1

Description: A homomorphism of left modules has a left module as domain. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Assertion	lmhmlmod1	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to S\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(S\right)$$
2		eqid	$$⊢\mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(T\right)$$
3	1 2	lmhmlem	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to \left(\left(S\in \mathrm{LMod}\wedge T\in \mathrm{LMod}\right)\wedge \left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(S\right)\right)\right)$$
4	3	simplld	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to S\in \mathrm{LMod}$$