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 )