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∈NrmVec→W∈TopVec

Proof

Step Hyp Ref Expression
1 nvcnlm ⊢W∈NrmVec→W∈NrmMod
2 nlmtlm ⊢W∈NrmMod→W∈TopMod
3 1 2 syl ⊢W∈NrmVec→W∈TopMod
4 eqid ⊢Scalar⁡W=Scalar⁡W
5 4 nlmnrg ⊢W∈NrmMod→Scalar⁡W∈NrmRing
6 1 5 syl ⊢W∈NrmVec→Scalar⁡W∈NrmRing
7 nvclvec ⊢W∈NrmVec→W∈LVec
8 4 lvecdrng ⊢W∈LVec→Scalar⁡W∈DivRing
9 7 8 syl ⊢W∈NrmVec→Scalar⁡W∈DivRing
10 nrgtdrg ⊢Scalar⁡W∈NrmRing∧Scalar⁡W∈DivRing→Scalar⁡W∈TopDRing
11 6 9 10 syl2anc ⊢W∈NrmVec→Scalar⁡W∈TopDRing
12 4 istvc ⊢W∈TopVec↔W∈TopMod∧Scalar⁡W∈TopDRing
13 3 11 12 sylanbrc ⊢W∈NrmVec→W∈TopVec