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

Definition df-tsms 21647
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 14138) and Σg (df-gsum 15814), 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 21646 . 2 class tsums
2 vw . . 3 setvar 𝑤
3 vf . . 3 setvar 𝑓
4 cvv 3077 . . 3 class V
5 vs . . . 4 setvar 𝑠
63cv 1473 . . . . . . 7 class 𝑓
76cdm 4932 . . . . . 6 class dom 𝑓
87cpw 4011 . . . . 5 class 𝒫 dom 𝑓
9 cfn 7721 . . . . 5 class Fin
108, 9cin 3443 . . . 4 class (𝒫 dom 𝑓 ∩ Fin)
11 vy . . . . . 6 setvar 𝑦
125cv 1473 . . . . . 6 class 𝑠
132cv 1473 . . . . . . 7 class 𝑤
1411cv 1473 . . . . . . . 8 class 𝑦
156, 14cres 4934 . . . . . . 7 class (𝑓𝑦)
16 cgsu 15812 . . . . . . 7 class Σg
1713, 15, 16co 6431 . . . . . 6 class (𝑤 Σg (𝑓𝑦))
1811, 12, 17cmpt 4541 . . . . 5 class (𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))
19 ctopn 15793 . . . . . . 7 class TopOpen
2013, 19cfv 5694 . . . . . 6 class (TopOpen‘𝑤)
21 vz . . . . . . . . 9 setvar 𝑧
2221cv 1473 . . . . . . . . . . 11 class 𝑧
2322, 14wss 3444 . . . . . . . . . 10 wff 𝑧𝑦
2423, 11, 12crab 2804 . . . . . . . . 9 class {𝑦𝑠𝑧𝑦}
2521, 12, 24cmpt 4541 . . . . . . . 8 class (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})
2625crn 4933 . . . . . . 7 class ran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})
27 cfg 19464 . . . . . . 7 class filGen
2812, 26, 27co 6431 . . . . . 6 class (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦}))
29 cflf 21456 . . . . . 6 class fLimf
3020, 28, 29co 6431 . . . . 5 class ((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))
3118, 30cfv 5694 . . . 4 class (((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))))
325, 10, 31csb 3403 . . 3 class (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦))))
332, 3, 4, 4, 32cmpt2 6433 . 2 class (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
341, 33wceq 1474 1 wff tsums = (𝑤 ∈ V, 𝑓 ∈ V ↦ (𝒫 dom 𝑓 ∩ Fin) / 𝑠(((TopOpen‘𝑤) fLimf (𝑠filGenran (𝑧𝑠 ↦ {𝑦𝑠𝑧𝑦})))‘(𝑦𝑠 ↦ (𝑤 Σg (𝑓𝑦)))))
Colors of variables: wff setvar class
This definition is referenced by:  tsmsval2  21650
  Copyright terms: Public domain W3C validator