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 = ( Scalar ` S )
	lmhmlem.l	|- L = ( Scalar ` T )
Assertion	lmhmsca	|- ( F e. ( S LMHom T ) -> L = K )

Proof

Step	Hyp	Ref	Expression
1		lmhmlem.k	|- K = ( Scalar ` S )
2		lmhmlem.l	|- L = ( Scalar ` T )
3	1 2	lmhmlem	|- ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ L = K ) ) )
4	3	simprrd	|- ( F e. ( S LMHom T ) -> L = K )