Metamath Proof Explorer

Theorem nmhmrcl1

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

Ref Expression
Assertion nmhmrcl1 ⊢ F ∈ S NMHom T → S ∈ 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 simpld ⊢ F ∈ S NMHom T → S ∈ NrmMod