Metamath Proof Explorer

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 S LMHom T L = K


Step Hyp Ref Expression
1 lmhmlem.k K = Scalar S
2 lmhmlem.l L = Scalar T
3 1 2 lmhmlem F S LMHom T S LMod T LMod F S GrpHom T L = K
4 3 simprrd F S LMHom T L = K