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 = ( 𝑤 ∈ 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 ( 𝑓𝑦 ) ) ) ) )