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

Metamath Proof Explorer

Theorem tsmsval

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmsval.b ⊢ B = Base G
tsmsval.j ⊢ J = TopOpen ⁡ G
tsmsval.s ⊢ S = 𝒫 A ∩ Fin
tsmsval.l ⊢ L = ran ⁡ z ∈ S ⟼ y ∈ S | z ⊆ y
tsmsval.g ⊢ φ → G ∈ V
tsmsval.a ⊢ φ → A ∈ W
tsmsval.f ⊢ φ → F : A ⟶ B
Assertion tsmsval ⊢ φ → G tsums F = J fLimf S filGen L ⁡ y ∈ S ⟼ ∑ G F ↾ y

Proof

Step Hyp Ref Expression
1 tsmsval.b ⊢ B = Base G
2 tsmsval.j ⊢ J = TopOpen ⁡ G
3 tsmsval.s ⊢ S = 𝒫 A ∩ Fin
4 tsmsval.l ⊢ L = ran ⁡ z ∈ S ⟼ y ∈ S | z ⊆ y
5 tsmsval.g ⊢ φ → G ∈ V
6 tsmsval.a ⊢ φ → A ∈ W
7 tsmsval.f ⊢ φ → F : A ⟶ B
8 1 fvexi ⊢ B ∈ V
9 8 a1i ⊢ φ → B ∈ V
10 fex2 ⊢ F : A ⟶ B ∧ A ∈ W ∧ B ∈ V → F ∈ V
11 7 6 9 10 syl3anc ⊢ φ → F ∈ V
12 7 fdmd ⊢ φ → dom ⁡ F = A
13 1 2 3 4 5 11 12 tsmsval2 ⊢ φ → G tsums F = J fLimf S filGen L ⁡ y ∈ S ⟼ ∑ G F ↾ y