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 )