Definition df-tsms 21930

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 14417) and gsum_g (df-gsum 16103), 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

Step	Hyp	Ref	Expression
1		ctsu 21929	. 2 class tsums
2		vw	. . 3 setvar w
3		vf	. . 3 setvar f
4		cvv 3200	. . 3 class _V
5		vs	. . . 4 setvar s
6	3	cv 1482	. . . . . . 7 class f
7	6	cdm 5114	. . . . . 6 class dom f
8	7	cpw 4158	. . . . 5 class ~P dom f
9		cfn 7955	. . . . 5 class Fin
10	8, 9	cin 3573	. . . 4 class ( ~P dom f i^i Fin )
11		vy	. . . . . 6 setvar y
12	5	cv 1482	. . . . . 6 class s
13	2	cv 1482	. . . . . . 7 class w
14	11	cv 1482	. . . . . . . 8 class y
15	6, 14	cres 5116	. . . . . . 7 class ( f |` y )
16		cgsu 16101	. . . . . . 7 class gsumg
17	13, 15, 16	co 6650	. . . . . 6 class ( w gsumg ( f |` y ) )
18	11, 12, 17	cmpt 4729	. . . . 5 class ( y e. s |-> ( w gsumg ( f |` y ) ) )
19		ctopn 16082	. . . . . . 7 class TopOpen
20	13, 19	cfv 5888	. . . . . 6 class ( TopOpen ` w )
21		vz	. . . . . . . . 9 setvar z
22	21	cv 1482	. . . . . . . . . . 11 class z
23	22, 14	wss 3574	. . . . . . . . . 10 wff z C_ y
24	23, 11, 12	crab 2916	. . . . . . . . 9 class { y e. s | z C_ y }
25	21, 12, 24	cmpt 4729	. . . . . . . 8 class ( z e. s |-> { y e. s | z C_ y } )
26	25	crn 5115	. . . . . . 7 class ran ( z e. s |-> { y e. s | z C_ y } )
27		cfg 19735	. . . . . . 7 class filGen
28	12, 26, 27	co 6650	. . . . . 6 class ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) )
29		cflf 21739	. . . . . 6 class fLimf
30	20, 28, 29	co 6650	. . . . 5 class ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) )
31	18, 30	cfv 5888	. . . 4 class ( ( ( TopOpen ` w ) fLimf ( s filGen ran ( z e. s |-> { y e. s | z C_ y } ) ) ) ` ( y e. s |-> ( w gsumg ( f |` y ) ) ) )
32	5, 10, 31	csb 3533	. . 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 ) ) ) )
33	2, 3, 4, 4, 32	cmpt2 6652	. 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 ) ) ) ) )
34	1, 33	wceq 1483	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 ) ) ) ) )

This definition is referenced by:  tsmsval2  21933