Metamath Proof Explorer

Theorem tsmscl

Description: A sum in a topological group is an element of the group. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmscl.b ⊢ B = Base G
tsmscl.1 ⊢ φ → G ∈ CMnd
tsmscl.2 ⊢ φ → G ∈ TopSp
tsmscl.a ⊢ φ → A ∈ V
tsmscl.f ⊢ φ → F : A ⟶ B
Assertion tsmscl ⊢ φ → G tsums F ⊆ B

Proof

Step Hyp Ref Expression
1 tsmscl.b ⊢ B = Base G
2 tsmscl.1 ⊢ φ → G ∈ CMnd
3 tsmscl.2 ⊢ φ → G ∈ TopSp
4 tsmscl.a ⊢ φ → A ∈ V
5 tsmscl.f ⊢ φ → F : A ⟶ B
6 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
7 eqid ⊢ 𝒫 A ∩ Fin = 𝒫 A ∩ Fin
8 1 6 7 2 3 4 5 eltsms ⊢ φ → x ∈ G tsums F ↔ x ∈ B ∧ ∀ w ∈ TopOpen ⁡ G x ∈ w → ∃ z ∈ 𝒫 A ∩ Fin ∀ y ∈ 𝒫 A ∩ Fin z ⊆ y → ∑ G F ↾ y ∈ w
9 simpl ⊢ x ∈ B ∧ ∀ w ∈ TopOpen ⁡ G x ∈ w → ∃ z ∈ 𝒫 A ∩ Fin ∀ y ∈ 𝒫 A ∩ Fin z ⊆ y → ∑ G F ↾ y ∈ w → x ∈ B
10 8 9 biimtrdi ⊢ φ → x ∈ G tsums F → x ∈ B
11 10 ssrdv ⊢ φ → G tsums F ⊆ B