Metamath Proof Explorer

Theorem nlmtlm

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

Ref Expression
Assertion nlmtlm ⊢ W ∈ NrmMod → W ∈ TopMod

Proof

Step Hyp Ref Expression
1 nlmngp ⊢ W ∈ NrmMod → W ∈ NrmGrp
2 nlmlmod ⊢ W ∈ NrmMod → W ∈ LMod
3 lmodabl ⊢ W ∈ LMod → W ∈ Abel
4 2 3 syl ⊢ W ∈ NrmMod → W ∈ Abel
5 ngptgp ⊢ W ∈ NrmGrp ∧ W ∈ Abel → W ∈ TopGrp
6 1 4 5 syl2anc ⊢ W ∈ NrmMod → W ∈ TopGrp
7 tgptmd ⊢ W ∈ TopGrp → W ∈ TopMnd
8 6 7 syl ⊢ W ∈ NrmMod → W ∈ TopMnd
9 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
10 9 nlmnrg ⊢ W ∈ NrmMod → Scalar ⁡ W ∈ NrmRing
11 nrgtrg ⊢ Scalar ⁡ W ∈ NrmRing → Scalar ⁡ W ∈ TopRing
12 10 11 syl ⊢ W ∈ NrmMod → Scalar ⁡ W ∈ TopRing
13 8 2 12 3jca ⊢ W ∈ NrmMod → W ∈ TopMnd ∧ W ∈ LMod ∧ Scalar ⁡ W ∈ TopRing
14 eqid ⊢ ⋅ 𝑠𝑓 ⁡ W = ⋅ 𝑠𝑓 ⁡ W
15 eqid ⊢ TopOpen ⁡ W = TopOpen ⁡ W
16 eqid ⊢ TopOpen ⁡ Scalar ⁡ W = TopOpen ⁡ Scalar ⁡ W
17 9 14 15 16 nlmvscn ⊢ W ∈ NrmMod → ⋅ 𝑠𝑓 ⁡ W ∈ TopOpen ⁡ Scalar ⁡ W × t TopOpen ⁡ W Cn TopOpen ⁡ W
18 14 15 9 16 istlm ⊢ W ∈ TopMod ↔ W ∈ TopMnd ∧ W ∈ LMod ∧ Scalar ⁡ W ∈ TopRing ∧ ⋅ 𝑠𝑓 ⁡ W ∈ TopOpen ⁡ Scalar ⁡ W × t TopOpen ⁡ W Cn TopOpen ⁡ W
19 13 17 18 sylanbrc ⊢ W ∈ NrmMod → W ∈ TopMod