Metamath Proof Explorer

Theorem nmhmnghm

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

Ref Expression
Assertion nmhmnghm ⊢ F ∈ S NMHom T → F ∈ S NGHom T

Proof

Step Hyp Ref Expression
1 isnmhm ⊢ F ∈ S NMHom T ↔ S ∈ NrmMod ∧ T ∈ NrmMod ∧ F ∈ S LMHom T ∧ F ∈ S NGHom T
2 1 simprbi ⊢ F ∈ S NMHom T → F ∈ S LMHom T ∧ F ∈ S NGHom T
3 2 simprd ⊢ F ∈ S NMHom T → F ∈ S NGHom T