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

Metamath Proof Explorer

Theorem tvctlm

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

Ref Expression
Assertion tvctlm ⊢ W ∈ TopVec → W ∈ TopMod

Proof

Step Hyp Ref Expression
1 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
2 1 istvc ⊢ W ∈ TopVec ↔ W ∈ TopMod ∧ Scalar ⁡ W ∈ TopDRing
3 2 simplbi ⊢ W ∈ TopVec → W ∈ TopMod