Metamath Proof Explorer

Definition df-tsms

Description: Define the set of limit points of an infinite group sum for the topological group G . If G is Hausdorff, then there will be at most one element in this set and U. ( W tsums F ) selects this unique element if it exists. ( W tsums F ) ~1o is a way to say that the sum exists and is unique. Note that unlike sum_ ( df-sum ) and gsum ( df-gsum ), this does not return the sum itself, but rather the set of all such sums, which is usually either empty or a singleton. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion df-tsms 
|- tsums = ( w e. _V , f e. _V |-> [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsu 
 |-  tsums
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vf 
 |-  f
4 3 cv 
 |-  f
5 4 cdm 
 |-  dom f
6 5 cpw 
 |-  ~P dom f
7 cfn 
 |-  Fin
8 6 7 cin 
 |-  ( ~P dom f i^i Fin )
9 vs 
 |-  s
10 ctopn 
 |-  TopOpen
11 1 cv 
 |-  w
12 11 10 cfv 
 |-  ( TopOpen ` w )
13 cflf 
 |-  fLimf
14 9 cv 
 |-  s
15 cfg 
 |-  filGen
16 vz 
 |-  z
17 vy 
 |-  y
18 16 cv 
 |-  z
19 17 cv 
 |-  y
20 18 19 wss 
 |-  z C_ y
21 20 17 14 crab 
 |-  { y e. s | z C_ y }
22 16 14 21 cmpt 
 |-  ( z e. s |-> { y e. s | z C_ y } )
23 22 crn 
 |-  ran ( z e. s |-> { y e. s | z C_ y } )
24 14 23 15 co 
 |-  ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) )
25 12 24 13 co 
 |-  ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) )
26 cgsu 
 |-  gsum
27 4 19 cres 
 |-  ( f |` y )
28 11 27 26 co 
 |-  ( w gsum ( f |` y ) )
29 17 14 28 cmpt 
 |-  ( y e. s |-> ( w gsum ( f |` y ) ) )
30 29 25 cfv 
 |-  ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) )
31 9 8 30 csb 
 |-  [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) )
32 1 3 2 2 31 cmpo 
 |-  ( w e. _V , f e. _V |-> [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) )
33 0 32 wceq 
 |-  tsums = ( w e. _V , f e. _V |-> [_ ( ~P dom f i^i Fin ) / s ]_ ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsum ( f |` y ) ) ) ) )