Description: Reverse closure for a normed module homomorphism. (Contributed by Mario Carneiro, 18-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | nmhmrcl2 | |- ( F e. ( S NMHom T ) -> T e. NrmMod ) |
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 | simprd | |- ( F e. ( S NMHom T ) -> T e. NrmMod ) |