Theorem nmhmghm

Description: A normed module homomorphism is a group homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

	Ref	Expression
Assertion	nmhmghm	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		nmhmnghm	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) )
2		nghmghm	⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
3	1 2	syl	⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )