Theorem lmhmsca

Description: A homomorphism of left modules constrains both modules to the same ring of scalars. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Hypotheses	lmhmlem.k	$$⊢K=\mathrm{Scalar}\left(S\right)$$
	lmhmlem.l	$$⊢L=\mathrm{Scalar}\left(T\right)$$
Assertion	lmhmsca	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to L=K$$

Proof

Step	Hyp	Ref	Expression
1		lmhmlem.k	$$⊢K=\mathrm{Scalar}\left(S\right)$$
2		lmhmlem.l	$$⊢L=\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 L=K\right)\right)$$
4	3	simprrd	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to L=K$$