Theorem tlmlmod

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

	Ref	Expression
Assertion	tlmlmod	⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ LMod )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ·sf ‘ 𝑊 ) = ( ·sf ‘ 𝑊 )
2		eqid	⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 )
3		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4		eqid	⊢ ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) = ( TopOpen ‘ ( Scalar ‘ 𝑊 ) )
5	1 2 3 4	istlm	⊢ ( 𝑊 ∈ TopMod ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ TopRing ) ∧ ( ·sf ‘ 𝑊 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) ×t ( TopOpen ‘ 𝑊 ) ) Cn ( TopOpen ‘ 𝑊 ) ) ) )
6	5	simplbi	⊢ ( 𝑊 ∈ TopMod → ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ TopRing ) )
7	6	simp2d	⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ LMod )