Metamath Proof Explorer


Theorem nvctvc

Description: A normed vector space is a topological vector space. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion nvctvc
|- ( W e. NrmVec -> W e. TopVec )

Proof

Step Hyp Ref Expression
1 nvcnlm
 |-  ( W e. NrmVec -> W e. NrmMod )
2 nlmtlm
 |-  ( W e. NrmMod -> W e. TopMod )
3 1 2 syl
 |-  ( W e. NrmVec -> W e. TopMod )
4 eqid
 |-  ( Scalar ` W ) = ( Scalar ` W )
5 4 nlmnrg
 |-  ( W e. NrmMod -> ( Scalar ` W ) e. NrmRing )
6 1 5 syl
 |-  ( W e. NrmVec -> ( Scalar ` W ) e. NrmRing )
7 nvclvec
 |-  ( W e. NrmVec -> W e. LVec )
8 4 lvecdrng
 |-  ( W e. LVec -> ( Scalar ` W ) e. DivRing )
9 7 8 syl
 |-  ( W e. NrmVec -> ( Scalar ` W ) e. DivRing )
10 nrgtdrg
 |-  ( ( ( Scalar ` W ) e. NrmRing /\ ( Scalar ` W ) e. DivRing ) -> ( Scalar ` W ) e. TopDRing )
11 6 9 10 syl2anc
 |-  ( W e. NrmVec -> ( Scalar ` W ) e. TopDRing )
12 4 istvc
 |-  ( W e. TopVec <-> ( W e. TopMod /\ ( Scalar ` W ) e. TopDRing ) )
13 3 11 12 sylanbrc
 |-  ( W e. NrmVec -> W e. TopVec )