Metamath Proof Explorer

Theorem tvclvec

Description: A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion tvclvec ⊢ W ∈ TopVec → W ∈ LVec

Proof

Step Hyp Ref Expression
1 tvclmod ⊢ W ∈ TopVec → W ∈ LMod
2 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
3 2 tvctdrg ⊢ W ∈ TopVec → Scalar ⁡ W ∈ TopDRing
4 tdrgdrng ⊢ Scalar ⁡ W ∈ TopDRing → Scalar ⁡ W ∈ DivRing
5 3 4 syl ⊢ W ∈ TopVec → Scalar ⁡ W ∈ DivRing
6 2 islvec ⊢ W ∈ LVec ↔ W ∈ LMod ∧ Scalar ⁡ W ∈ DivRing
7 1 5 6 sylanbrc ⊢ W ∈ TopVec → W ∈ LVec