Metamath Proof Explorer

Theorem tsmsid

Description: If a sum is finite, the usual sum is always a limit point of the topological sum (although it may not be the only limit point). (Contributed by Mario Carneiro, 2-Sep-2015) (Revised by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsid.b 
|- B = ( Base ` G )
tsmsid.z 
|- .0. = ( 0g ` G )
tsmsid.1 
|- ( ph -> G e. CMnd )
tsmsid.2 
|- ( ph -> G e. TopSp )
tsmsid.a 
|- ( ph -> A e. V )
tsmsid.f 
|- ( ph -> F : A --> B )
tsmsid.w 
|- ( ph -> F finSupp .0. )
Assertion tsmsid 
|- ( ph -> ( G gsum F ) e. ( G tsums F ) )

Proof

Step Hyp Ref Expression
1 tsmsid.b 
 |-  B = ( Base ` G )
2 tsmsid.z 
 |-  .0. = ( 0g ` G )
3 tsmsid.1 
 |-  ( ph -> G e. CMnd )
4 tsmsid.2 
 |-  ( ph -> G e. TopSp )
5 tsmsid.a 
 |-  ( ph -> A e. V )
6 tsmsid.f 
 |-  ( ph -> F : A --> B )
7 tsmsid.w 
 |-  ( ph -> F finSupp .0. )
8 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
9 1 8 istps 
 |-  ( G e. TopSp <-> ( TopOpen ` G ) e. ( TopOn ` B ) )
10 4 9 sylib 
 |-  ( ph -> ( TopOpen ` G ) e. ( TopOn ` B ) )
11 topontop 
 |-  ( ( TopOpen ` G ) e. ( TopOn ` B ) -> ( TopOpen ` G ) e. Top )
12 10 11 syl 
 |-  ( ph -> ( TopOpen ` G ) e. Top )
13 1 2 3 5 6 7 gsumcl 
 |-  ( ph -> ( G gsum F ) e. B )
14 13 snssd 
 |-  ( ph -> { ( G gsum F ) } C_ B )
15 toponuni 
 |-  ( ( TopOpen ` G ) e. ( TopOn ` B ) -> B = U. ( TopOpen ` G ) )
16 10 15 syl 
 |-  ( ph -> B = U. ( TopOpen ` G ) )
17 14 16 sseqtrd 
 |-  ( ph -> { ( G gsum F ) } C_ U. ( TopOpen ` G ) )
18 eqid 
 |-  U. ( TopOpen ` G ) = U. ( TopOpen ` G )
19 18 sscls 
 |-  ( ( ( TopOpen ` G ) e. Top /\ { ( G gsum F ) } C_ U. ( TopOpen ` G ) ) -> { ( G gsum F ) } C_ ( ( cls ` ( TopOpen ` G ) ) ` { ( G gsum F ) } ) )
20 12 17 19 syl2anc 
 |-  ( ph -> { ( G gsum F ) } C_ ( ( cls ` ( TopOpen ` G ) ) ` { ( G gsum F ) } ) )
21 ovex 
 |-  ( G gsum F ) e. _V
22 21 snss 
 |-  ( ( G gsum F ) e. ( ( cls ` ( TopOpen ` G ) ) ` { ( G gsum F ) } ) <-> { ( G gsum F ) } C_ ( ( cls ` ( TopOpen ` G ) ) ` { ( G gsum F ) } ) )
23 20 22 sylibr 
 |-  ( ph -> ( G gsum F ) e. ( ( cls ` ( TopOpen ` G ) ) ` { ( G gsum F ) } ) )
24 1 2 3 4 5 6 7 8 tsmsgsum 
 |-  ( ph -> ( G tsums F ) = ( ( cls ` ( TopOpen ` G ) ) ` { ( G gsum F ) } ) )
25 23 24 eleqtrrd 
 |-  ( ph -> ( G gsum F ) e. ( G tsums F ) )