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