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

Definition df-tsms 21740
 Description: Define the set of limit points of an infinite group sum for the topological group 𝐺. If 𝐺 is Hausdorff, then there will be at most one element in this set and ∪ (𝑊 tsums 𝐹) selects this unique element if it exists. (𝑊 tsums 𝐹) ≈ 1𝑜 is a way to say that the sum exists and is unique. Note that unlike Σ (df-sum 14265) and Σg (df-gsum 15926), 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 = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
Distinct variable group:   𝑓,𝑠,𝑤,𝑦,𝑧

Detailed syntax breakdown of Definition df-tsms
StepHypRef Expression
1 ctsu 21739 . 2 class tsums
2 vw . . 3 setvar 𝑤
3 vf . . 3 setvar 𝑓
4 cvv 3173 . . 3 class V
5 vs . . . 4 setvar 𝑠
63cv 1474 . . . . . . 7 class 𝑓
76cdm 5038 . . . . . 6 class dom 𝑓
87cpw 4108 . . . . 5 class 𝒫 dom 𝑓
9 cfn 7841 . . . . 5 class Fin
108, 9cin 3539 . . . 4 class (𝒫 dom 𝑓 ∩ Fin)
11 vy . . . . . 6 setvar 𝑦
125cv 1474 . . . . . 6 class 𝑠
132cv 1474 . . . . . . 7 class 𝑤
1411cv 1474 . . . . . . . 8 class 𝑦
156, 14cres 5040 . . . . . . 7 class (𝑓𝑦)
16 cgsu 15924 . . . . . . 7 class Σg
1713, 15, 16co 6549 . . . . . 6 class (𝑤 Σg (𝑓𝑦))
1811, 12, 17cmpt 4643 . . . . 5 class (𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))
19 ctopn 15905 . . . . . . 7 class TopOpen
2013, 19cfv 5804 . . . . . 6 class (TopOpen‘𝑤)
21 vz . . . . . . . . 9 setvar 𝑧
2221cv 1474 . . . . . . . . . . 11 class 𝑧
2322, 14wss 3540 . . . . . . . . . 10 wff 𝑧𝑦
2423, 11, 12crab 2900 . . . . . . . . 9 class {𝑦𝑠𝑧𝑦}
2521, 12, 24cmpt 4643 . . . . . . . 8 class (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})
2625crn 5039 . . . . . . 7 class ran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})
27 cfg 19556 . . . . . . 7 class filGen
2812, 26, 27co 6549 . . . . . 6 class (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}))
29 cflf 21549 . . . . . 6 class fLimf
3020, 28, 29co 6549 . . . . 5 class ((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))
3118, 30cfv 5804 . . . 4 class (((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))))
325, 10, 31csb 3499 . . 3 class (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))))
332, 3, 4, 4, 32cmpt2 6551 . 2 class (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
341, 33wceq 1475 1 wff tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
 Colors of variables: wff setvar class This definition is referenced by:  tsmsval2  21743
 Copyright terms: Public domain W3C validator