This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑊 ∈ NrmVec → 𝑊 ∈ TopVec )

Proof

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