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 = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctsu	⊢ tsums
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vf	⊢ 𝑓
4	3	cv	⊢ 𝑓
5	4	cdm	⊢ dom 𝑓
6	5	cpw	⊢ 𝒫 dom 𝑓
7		cfn	⊢ Fin
8	6 7	cin	⊢ ( 𝒫 dom 𝑓 ∩ Fin )
9		vs	⊢ 𝑠
10		ctopn	⊢ TopOpen
11	1	cv	⊢ 𝑤
12	11 10	cfv	⊢ ( TopOpen ‘ 𝑤 )
13		cflf	⊢ fLimf
14	9	cv	⊢ 𝑠
15		cfg	⊢ filGen
16		vz	⊢ 𝑧
17		vy	⊢ 𝑦
18	16	cv	⊢ 𝑧
19	17	cv	⊢ 𝑦
20	18 19	wss	⊢ 𝑧 ⊆ 𝑦
21	20 17 14	crab	⊢ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 }
22	16 14 21	cmpt	⊢ ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } )
23	22	crn	⊢ ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } )
24	14 23 15	co	⊢ ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) )
25	12 24 13	co	⊢ ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) )
26		cgsu	⊢ Σg
27	4 19	cres	⊢ ( 𝑓 ↾ 𝑦 )
28	11 27 26	co	⊢ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) )
29	17 14 28	cmpt	⊢ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) )
30	29 25	cfv	⊢ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) )
31	9 8 30	csb	⊢ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) )
32	1 3 2 2 31	cmpo	⊢ ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) )
33	0 32	wceq	⊢ tsums = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) )