Metamath Proof Explorer

Theorem tlmlmod

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

Ref Expression
Assertion tlmlmod ⊢ W ∈ TopMod → W ∈ LMod

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋅ 𝑠𝑓 ⁡ W = ⋅ 𝑠𝑓 ⁡ W
2 eqid ⊢ TopOpen ⁡ W = TopOpen ⁡ W
3 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
4 eqid ⊢ TopOpen ⁡ Scalar ⁡ W = TopOpen ⁡ Scalar ⁡ W
5 1 2 3 4 istlm ⊢ W ∈ TopMod ↔ W ∈ TopMnd ∧ W ∈ LMod ∧ Scalar ⁡ W ∈ TopRing ∧ ⋅ 𝑠𝑓 ⁡ W ∈ TopOpen ⁡ Scalar ⁡ W × t TopOpen ⁡ W Cn TopOpen ⁡ W
6 5 simplbi ⊢ W ∈ TopMod → W ∈ TopMnd ∧ W ∈ LMod ∧ Scalar ⁡ W ∈ TopRing
7 6 simp2d ⊢ W ∈ TopMod → W ∈ LMod