Metamath Proof Explorer

Theorem lmghm

Description: A homomorphism of left modules is a homomorphism of groups. (Contributed by Stefan O'Rear, 1-Jan-2015)

Ref Expression
Assertion lmghm 
|- ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )

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 simprld 
 |-  ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )