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 )