Metamath Proof Explorer


Theorem lmhmlmod2

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

Ref Expression
Assertion lmhmlmod2 FSLMHomTTLMod

Proof

Step Hyp Ref Expression
1 eqid ScalarS=ScalarS
2 eqid ScalarT=ScalarT
3 1 2 lmhmlem FSLMHomTSLModTLModFSGrpHomTScalarT=ScalarS
4 3 simplrd FSLMHomTTLMod