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 ∈ V , f ∈ V ⟼ ⦋ 𝒫 dom ⁡ f ∩ Fin / s⦌ TopOpen ⁡ w fLimf s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y ⁡ y ∈ s ⟼ ∑ w f ↾ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctsu class tsums
1 vw setvar w
2 cvv class V
3 vf setvar f
4 3 cv setvar f
5 4 cdm class dom ⁡ f
6 5 cpw class 𝒫 dom ⁡ f
7 cfn class Fin
8 6 7 cin class 𝒫 dom ⁡ f ∩ Fin
9 vs setvar s
10 ctopn class TopOpen
11 1 cv setvar w
12 11 10 cfv class TopOpen ⁡ w
13 cflf class fLimf
14 9 cv setvar s
15 cfg class filGen
16 vz setvar z
17 vy setvar y
18 16 cv setvar z
19 17 cv setvar y
20 18 19 wss wff z ⊆ y
21 20 17 14 crab class y ∈ s | z ⊆ y
22 16 14 21 cmpt class z ∈ s ⟼ y ∈ s | z ⊆ y
23 22 crn class ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y
24 14 23 15 co class s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y
25 12 24 13 co class TopOpen ⁡ w fLimf s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y
26 cgsu class Σ𝑔
27 4 19 cres class f ↾ y
28 11 27 26 co class ∑ w f ↾ y
29 17 14 28 cmpt class y ∈ s ⟼ ∑ w f ↾ y
30 29 25 cfv class TopOpen ⁡ w fLimf s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y ⁡ y ∈ s ⟼ ∑ w f ↾ y
31 9 8 30 csb class ⦋ 𝒫 dom ⁡ f ∩ Fin / s⦌ TopOpen ⁡ w fLimf s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y ⁡ y ∈ s ⟼ ∑ w f ↾ y
32 1 3 2 2 31 cmpo class w ∈ V , f ∈ V ⟼ ⦋ 𝒫 dom ⁡ f ∩ Fin / s⦌ TopOpen ⁡ w fLimf s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y ⁡ y ∈ s ⟼ ∑ w f ↾ y
33 0 32 wceq wff tsums = w ∈ V , f ∈ V ⟼ ⦋ 𝒫 dom ⁡ f ∩ Fin / s⦌ TopOpen ⁡ w fLimf s filGen ran ⁡ z ∈ s ⟼ y ∈ s | z ⊆ y ⁡ y ∈ s ⟼ ∑ w f ↾ y