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

Proof

Step Hyp Ref Expression
1 nmhmnghm 
 |-  ( F e. ( S NMHom T ) -> F e. ( S NGHom T ) )
2 nghmghm 
 |-  ( F e. ( S NGHom T ) -> F e. ( S GrpHom T ) )
3 1 2 syl 
 |-  ( F e. ( S NMHom T ) -> F e. ( S GrpHom T ) )