Metamath Proof Explorer

Theorem haustsms

Description: In a Hausdorff topological group, a sum has at most one limit point. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmscl.b 
|- B = ( Base ` G )
tsmscl.1 
|- ( ph -> G e. CMnd )
tsmscl.2 
|- ( ph -> G e. TopSp )
tsmscl.a 
|- ( ph -> A e. V )
tsmscl.f 
|- ( ph -> F : A --> B )
haustsms.j 
|- J = ( TopOpen ` G )
haustsms.h 
|- ( ph -> J e. Haus )
Assertion haustsms 
|- ( ph -> E* x x e. ( G tsums F ) )

Proof

Step Hyp Ref Expression
1 tsmscl.b 
 |-  B = ( Base ` G )
2 tsmscl.1 
 |-  ( ph -> G e. CMnd )
3 tsmscl.2 
 |-  ( ph -> G e. TopSp )
4 tsmscl.a 
 |-  ( ph -> A e. V )
5 tsmscl.f 
 |-  ( ph -> F : A --> B )
6 haustsms.j 
 |-  J = ( TopOpen ` G )
7 haustsms.h 
 |-  ( ph -> J e. Haus )
8 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
9 eqid 
 |-  ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } )
10 eqid 
 |-  ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } )
11 8 9 10 4 tsmsfbas 
 |-  ( ph -> ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) )
12 fgcl 
 |-  ( ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
13 11 12 syl 
 |-  ( ph -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
14 1 8 2 4 5 tsmslem1 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) e. B )
15 1 6 tpsuni 
 |-  ( G e. TopSp -> B = U. J )
16 3 15 syl 
 |-  ( ph -> B = U. J )
17 16 adantr 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> B = U. J )
18 14 17 eleqtrd 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) e. U. J )
19 18 fmpttd 
 |-  ( ph -> ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) : ( ~P A i^i Fin ) --> U. J )
20 eqid 
 |-  U. J = U. J
21 20 hausflf 
 |-  ( ( J e. Haus /\ ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) /\ ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) : ( ~P A i^i Fin ) --> U. J ) -> E* x x e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
22 7 13 19 21 syl3anc 
 |-  ( ph -> E* x x e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
23 1 6 8 10 2 4 5 tsmsval 
 |-  ( ph -> ( G tsums F ) = ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
24 23 eleq2d 
 |-  ( ph -> ( x e. ( G tsums F ) <-> x e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) )
25 24 mobidv 
 |-  ( ph -> ( E* x x e. ( G tsums F ) <-> E* x x e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) )
26 22 25 mpbird 
 |-  ( ph -> E* x x e. ( G tsums F ) )