Metamath Proof Explorer

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 e. ( S LMHom T ) -> S e. LMod )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Scalar ` S ) = ( Scalar ` S )
2 eqid 
 |-  ( Scalar ` T ) = ( Scalar ` T )
3 1 2 lmhmlem 
 |-  ( F e. ( S LMHom T ) -> ( ( S e. LMod /\ T e. LMod ) /\ ( F e. ( S GrpHom T ) /\ ( Scalar ` T ) = ( Scalar ` S ) ) ) )
4 3 simplld 
 |-  ( F e. ( S LMHom T ) -> S e. LMod )