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