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 e. NrmMod -> W e. TopMod )

Proof

Step Hyp Ref Expression
1 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
2 nlmlmod 
 |-  ( W e. NrmMod -> W e. LMod )
3 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
4 2 3 syl 
 |-  ( W e. NrmMod -> W e. Abel )
5 ngptgp 
 |-  ( ( W e. NrmGrp /\ W e. Abel ) -> W e. TopGrp )
6 1 4 5 syl2anc 
 |-  ( W e. NrmMod -> W e. TopGrp )
7 tgptmd 
 |-  ( W e. TopGrp -> W e. TopMnd )
8 6 7 syl 
 |-  ( W e. NrmMod -> W e. TopMnd )
9 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
10 9 nlmnrg 
 |-  ( W e. NrmMod -> ( Scalar ` W ) e. NrmRing )
11 nrgtrg 
 |-  ( ( Scalar ` W ) e. NrmRing -> ( Scalar ` W ) e. TopRing )
12 10 11 syl 
 |-  ( W e. NrmMod -> ( Scalar ` W ) e. TopRing )
13 8 2 12 3jca 
 |-  ( W e. NrmMod -> ( W e. TopMnd /\ W e. LMod /\ ( Scalar ` W ) e. TopRing ) )
14 eqid 
 |-  ( .sf ` W ) = ( .sf ` W )
15 eqid 
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
16 eqid 
 |-  ( TopOpen ` ( Scalar ` W ) ) = ( TopOpen ` ( Scalar ` W ) )
17 9 14 15 16 nlmvscn 
 |-  ( W e. NrmMod -> ( .sf ` W ) e. ( ( ( TopOpen ` ( Scalar ` W ) ) tX ( TopOpen ` W ) ) Cn ( TopOpen ` W ) ) )
18 14 15 9 16 istlm 
 |-  ( W e. TopMod <-> ( ( W e. TopMnd /\ W e. LMod /\ ( Scalar ` W ) e. TopRing ) /\ ( .sf ` W ) e. ( ( ( TopOpen ` ( Scalar ` W ) ) tX ( TopOpen ` W ) ) Cn ( TopOpen ` W ) ) ) )
19 13 17 18 sylanbrc 
 |-  ( W e. NrmMod -> W e. TopMod )