MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tsms Unicode version

Definition df-tsms 17825
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 12175) and  gsumg (df-gsum 13421), 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.)
Assertion
Ref Expression
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  gsumg  ( f  |`  y ) ) ) ) )
Distinct variable group:    f, s, w, y, z

Detailed syntax breakdown of Definition df-tsms
StepHypRef Expression
1 ctsu 17824 . 2  class tsums
2 vw . . 3  set  w
3 vf . . 3  set  f
4 cvv 2801 . . 3  class  _V
5 vs . . . 4  set  s
63cv 1631 . . . . . . 7  class  f
76cdm 4705 . . . . . 6  class  dom  f
87cpw 3638 . . . . 5  class  ~P dom  f
9 cfn 6879 . . . . 5  class  Fin
108, 9cin 3164 . . . 4  class  ( ~P
dom  f  i^i  Fin )
11 vy . . . . . 6  set  y
125cv 1631 . . . . . 6  class  s
132cv 1631 . . . . . . 7  class  w
1411cv 1631 . . . . . . . 8  class  y
156, 14cres 4707 . . . . . . 7  class  ( f  |`  y )
16 cgsu 13417 . . . . . . 7  class  gsumg
1713, 15, 16co 5874 . . . . . 6  class  ( w 
gsumg  ( f  |`  y
) )
1811, 12, 17cmpt 4093 . . . . 5  class  ( y  e.  s  |->  ( w 
gsumg  ( f  |`  y
) ) )
19 ctopn 13342 . . . . . . 7  class  TopOpen
2013, 19cfv 5271 . . . . . 6  class  ( TopOpen `  w )
21 vz . . . . . . . . 9  set  z
2221cv 1631 . . . . . . . . . . 11  class  z
2322, 14wss 3165 . . . . . . . . . 10  wff  z  C_  y
2423, 11, 12crab 2560 . . . . . . . . 9  class  { y  e.  s  |  z 
C_  y }
2521, 12, 24cmpt 4093 . . . . . . . 8  class  ( z  e.  s  |->  { y  e.  s  |  z 
C_  y } )
2625crn 4706 . . . . . . 7  class  ran  (
z  e.  s  |->  { y  e.  s  |  z  C_  y }
)
27 cfg 17535 . . . . . . 7  class  filGen
2812, 26, 27co 5874 . . . . . 6  class  ( s
filGen ran  ( z  e.  s  |->  { y  e.  s  |  z  C_  y } ) )
29 cflf 17646 . . . . . 6  class  fLimf
3020, 28, 29co 5874 . . . . 5  class  ( (
TopOpen `  w )  fLimf  ( s filGen ran  ( z  e.  s  |->  { y  e.  s  |  z 
C_  y } ) ) )
3118, 30cfv 5271 . . . 4  class  ( ( ( TopOpen `  w )  fLimf  ( s filGen ran  (
z  e.  s  |->  { y  e.  s  |  z  C_  y }
) ) ) `  ( y  e.  s 
|->  ( w  gsumg  ( f  |`  y
) ) ) )
325, 10, 31csb 3094 . . 3  class  [_ ( ~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  gsumg  ( f  |`  y ) ) ) )
332, 3, 4, 4, 32cmpt2 5876 . 2  class  ( 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  gsumg  ( f  |`  y ) ) ) ) )
341, 33wceq 1632 1  wff 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  gsumg  ( f  |`  y ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  tsmsval2  17828
  Copyright terms: Public domain W3C validator