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\in \left(S\mathrm{LMHom}T\right)\to F\in \left(S\mathrm{GrpHom}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{Scalar}\left(S\right)=\mathrm{Scalar}\left(S\right)$$
2		eqid	$$⊢\mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(T\right)$$
3	1 2	lmhmlem	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to \left(\left(S\in \mathrm{LMod}\wedge T\in \mathrm{LMod}\right)\wedge \left(F\in \left(S\mathrm{GrpHom}T\right)\wedge \mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(S\right)\right)\right)$$
4	3	simprld	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to F\in \left(S\mathrm{GrpHom}T\right)$$