Metamath Proof Explorer

Theorem nmhmrcl2

Description: Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)

Ref Expression
Assertion nmhmrcl2 ⊢ F ∈ S NMHom T → T ∈ NrmMod

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 simplbi ⊢ F ∈ S NMHom T → S ∈ NrmMod ∧ T ∈ NrmMod
3 2 simprd ⊢ F ∈ S NMHom T → T ∈ NrmMod