This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 isnmhm 
 |-  ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) )
2 1 simplbi 
 |-  ( F e. ( S NMHom T ) -> ( S e. NrmMod /\ T e. NrmMod ) )
3 2 simpld 
 |-  ( F e. ( S NMHom T ) -> S e. NrmMod )