Theorem lmhmghmd

Description: A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypothesis	lmhmghmd.1	$$⊢\phi \to F\in \left(S\mathrm{LMHom}T\right)$$
Assertion	lmhmghmd	$$⊢\phi \to F\in \left(S\mathrm{GrpHom}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		lmhmghmd.1	$$⊢\phi \to F\in \left(S\mathrm{LMHom}T\right)$$
2		lmghm	$$⊢F\in \left(S\mathrm{LMHom}T\right)\to F\in \left(S\mathrm{GrpHom}T\right)$$
3	1 2	syl	$$⊢\phi \to F\in \left(S\mathrm{GrpHom}T\right)$$