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×tTopOpen⁡WCnTopOpen⁡W
18 14 15 9 16 istlm ⊢W∈TopMod↔W∈TopMnd∧W∈LMod∧Scalar⁡W∈TopRing∧⋅𝑠𝑓⁡W∈TopOpen⁡Scalar⁡W×tTopOpen⁡WCnTopOpen⁡W
19 13 17 18 sylanbrc ⊢W∈NrmMod→W∈TopMod