Theorem tvctlm

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

	Ref	Expression
Assertion	tvctlm	⊢ ( 𝑊 ∈ TopVec → 𝑊 ∈ TopMod )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
2	1	istvc	⊢ ( 𝑊 ∈ TopVec ↔ ( 𝑊 ∈ TopMod ∧ ( Scalar ‘ 𝑊 ) ∈ TopDRing ) )
3	2	simplbi	⊢ ( 𝑊 ∈ TopVec → 𝑊 ∈ TopMod )