This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑓 ↾ 𝑦 ) ) ) ) )