Metamath Proof Explorer

Theorem nmhmghm

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

		Ref	Expression
	Assertion	nmhmghm	$⊢ F \in (S NMHom T) \to F \in (S GrpHom T)$

Step	Hyp	Ref	Expression
1		nmhmnghm	$⊢ F \in (S NMHom T) \to F \in (S NGHom T)$
2		nghmghm	$⊢ F \in (S NGHom T) \to F \in (S GrpHom T)$
3	1 2	syl	$⊢ F \in (S NMHom T) \to F \in (S GrpHom T)$