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	$$⊢\mathrm{tsums}=\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left(𝒫\mathrm{dom}f\cap \mathrm{Fin}\right)/s⦌\left(\mathrm{TopOpen}\left(w\right)\mathrm{fLimf}\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)\right)\left(\left(y\in s⟼{\sum }_w\left({f\upharpoonright }_y\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsu	$$class\mathrm{tsums}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4	3	cv	$$setvarf$$
5	4	cdm	$$class\mathrm{dom}f$$
6	5	cpw	$$class𝒫\mathrm{dom}f$$
7		cfn	$$class\mathrm{Fin}$$
8	6 7	cin	$$class\left(𝒫\mathrm{dom}f\cap \mathrm{Fin}\right)$$
9		vs	$$setvars$$
10		ctopn	$$class\mathrm{TopOpen}$$
11	1	cv	$$setvarw$$
12	11 10	cfv	$$class\mathrm{TopOpen}\left(w\right)$$
13		cflf	$$class\mathrm{fLimf}$$
14	9	cv	$$setvars$$
15		cfg	$$class\mathrm{filGen}$$
16		vz	$$setvarz$$
17		vy	$$setvary$$
18	16	cv	$$setvarz$$
19	17	cv	$$setvary$$
20	18 19	wss	$$wffz\subseteq y$$
21	20 17 14	crab	$$class\left\{y\in s|z\subseteq y\right\}$$
22	16 14 21	cmpt	$$class\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)$$
23	22	crn	$$class\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)$$
24	14 23 15	co	$$class\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)$$
25	12 24 13	co	$$class\left(\mathrm{TopOpen}\left(w\right)\mathrm{fLimf}\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)\right)$$
26		cgsu	$$class{\Sigma }_{𝑔}$$
27	4 19	cres	$$class\left({f\upharpoonright }_y\right)$$
28	11 27 26	co	$$class\left({\sum }_w,\left({f\upharpoonright }_y\right)\right)$$
29	17 14 28	cmpt	$$class\left(y\in s⟼{\sum }_w\left({f\upharpoonright }_y\right)\right)$$
30	29 25	cfv	$$class\left(\mathrm{TopOpen}\left(w\right)\mathrm{fLimf}\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)\right)\left(\left(y\in s⟼{\sum }_w\left({f\upharpoonright }_y\right)\right)\right)$$
31	9 8 30	csb	$$class⦋\left(𝒫\mathrm{dom}f\cap \mathrm{Fin}\right)/s⦌\left(\mathrm{TopOpen}\left(w\right)\mathrm{fLimf}\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)\right)\left(\left(y\in s⟼{\sum }_w\left({f\upharpoonright }_y\right)\right)\right)$$
32	1 3 2 2 31	cmpo	$$class\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left(𝒫\mathrm{dom}f\cap \mathrm{Fin}\right)/s⦌\left(\mathrm{TopOpen}\left(w\right)\mathrm{fLimf}\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)\right)\left(\left(y\in s⟼{\sum }_w\left({f\upharpoonright }_y\right)\right)\right)\right)$$
33	0 32	wceq	$$wff\mathrm{tsums}=\left(w\in \mathrm{V},f\in \mathrm{V}⟼⦋\left(𝒫\mathrm{dom}f\cap \mathrm{Fin}\right)/s⦌\left(\mathrm{TopOpen}\left(w\right)\mathrm{fLimf}\left(s\mathrm{filGen}\mathrm{ran}\left(z\in s⟼\left\{y\in s|z\subseteq y\right\}\right)\right)\right)\left(\left(y\in s⟼{\sum }_w\left({f\upharpoonright }_y\right)\right)\right)\right)$$