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

Metamath Proof Explorer

Theorem tgptsmscld

Description: The set of limit points to an infinite sum in a topological group is closed. (Contributed by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses tgptsmscls.b 
|- B = ( Base ` G )
tgptsmscls.j 
|- J = ( TopOpen ` G )
tgptsmscls.1 
|- ( ph -> G e. CMnd )
tgptsmscls.2 
|- ( ph -> G e. TopGrp )
tgptsmscls.a 
|- ( ph -> A e. V )
tgptsmscls.f 
|- ( ph -> F : A --> B )
Assertion tgptsmscld 
|- ( ph -> ( G tsums F ) e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 tgptsmscls.b 
 |-  B = ( Base ` G )
2 tgptsmscls.j 
 |-  J = ( TopOpen ` G )
3 tgptsmscls.1 
 |-  ( ph -> G e. CMnd )
4 tgptsmscls.2 
 |-  ( ph -> G e. TopGrp )
5 tgptsmscls.a 
 |-  ( ph -> A e. V )
6 tgptsmscls.f 
 |-  ( ph -> F : A --> B )
7 2 1 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` B ) )
8 4 7 syl 
 |-  ( ph -> J e. ( TopOn ` B ) )
9 topontop 
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
10 8 9 syl 
 |-  ( ph -> J e. Top )
11 0cld 
 |-  ( J e. Top -> (/) e. ( Clsd ` J ) )
12 10 11 syl 
 |-  ( ph -> (/) e. ( Clsd ` J ) )
13 eleq1 
 |-  ( ( G tsums F ) = (/) -> ( ( G tsums F ) e. ( Clsd ` J ) <-> (/) e. ( Clsd ` J ) ) )
14 12 13 syl5ibrcom 
 |-  ( ph -> ( ( G tsums F ) = (/) -> ( G tsums F ) e. ( Clsd ` J ) ) )
15 n0 
 |-  ( ( G tsums F ) =/= (/) <-> E. x x e. ( G tsums F ) )
16 3 adantr 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> G e. CMnd )
17 4 adantr 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> G e. TopGrp )
18 5 adantr 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> A e. V )
19 6 adantr 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> F : A --> B )
20 simpr 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> x e. ( G tsums F ) )
21 1 2 16 17 18 19 20 tgptsmscls 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> ( G tsums F ) = ( ( cls ` J ) ` { x } ) )
22 tgptps 
 |-  ( G e. TopGrp -> G e. TopSp )
23 4 22 syl 
 |-  ( ph -> G e. TopSp )
24 1 3 23 5 6 tsmscl 
 |-  ( ph -> ( G tsums F ) C_ B )
25 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
26 8 25 syl 
 |-  ( ph -> B = U. J )
27 24 26 sseqtrd 
 |-  ( ph -> ( G tsums F ) C_ U. J )
28 27 sselda 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> x e. U. J )
29 28 snssd 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> { x } C_ U. J )
30 eqid 
 |-  U. J = U. J
31 30 clscld 
 |-  ( ( J e. Top /\ { x } C_ U. J ) -> ( ( cls ` J ) ` { x } ) e. ( Clsd ` J ) )
32 10 29 31 syl2an2r 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> ( ( cls ` J ) ` { x } ) e. ( Clsd ` J ) )
33 21 32 eqeltrd 
 |-  ( ( ph /\ x e. ( G tsums F ) ) -> ( G tsums F ) e. ( Clsd ` J ) )
34 33 ex 
 |-  ( ph -> ( x e. ( G tsums F ) -> ( G tsums F ) e. ( Clsd ` J ) ) )
35 34 exlimdv 
 |-  ( ph -> ( E. x x e. ( G tsums F ) -> ( G tsums F ) e. ( Clsd ` J ) ) )
36 15 35 biimtrid 
 |-  ( ph -> ( ( G tsums F ) =/= (/) -> ( G tsums F ) e. ( Clsd ` J ) ) )
37 14 36 pm2.61dne 
 |-  ( ph -> ( G tsums F ) e. ( Clsd ` J ) )