This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nlmtlm

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

Ref Expression
Assertion nlmtlm ( 𝑊 ∈ NrmMod → 𝑊 ∈ TopMod )

Proof

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