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 ) ) ) ) )