Metamath Proof Explorer

Theorem tsmsid

Description: If a sum is finite, the usual sum is always a limit point of the topological sum (although it may not be the only limit point). (Contributed by Mario Carneiro, 2-Sep-2015) (Revised by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsid.b ⊢ B = Base G
tsmsid.z ⊢ 0 ˙ = 0 G
tsmsid.1 ⊢ φ → G ∈ CMnd
tsmsid.2 ⊢ φ → G ∈ TopSp
tsmsid.a ⊢ φ → A ∈ V
tsmsid.f ⊢ φ → F : A ⟶ B
tsmsid.w ⊢ φ → finSupp 0 ˙⁡ F
Assertion tsmsid ⊢ φ → ∑ G F ∈ G tsums F

Proof

Step Hyp Ref Expression
1 tsmsid.b ⊢ B = Base G
2 tsmsid.z ⊢ 0 ˙ = 0 G
3 tsmsid.1 ⊢ φ → G ∈ CMnd
4 tsmsid.2 ⊢ φ → G ∈ TopSp
5 tsmsid.a ⊢ φ → A ∈ V
6 tsmsid.f ⊢ φ → F : A ⟶ B
7 tsmsid.w ⊢ φ → finSupp 0 ˙⁡ F
8 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
9 1 8 istps ⊢ G ∈ TopSp ↔ TopOpen ⁡ G ∈ TopOn ⁡ B
10 4 9 sylib ⊢ φ → TopOpen ⁡ G ∈ TopOn ⁡ B
11 topontop ⊢ TopOpen ⁡ G ∈ TopOn ⁡ B → TopOpen ⁡ G ∈ Top
12 10 11 syl ⊢ φ → TopOpen ⁡ G ∈ Top
13 1 2 3 5 6 7 gsumcl ⊢ φ → ∑ G F ∈ B
14 13 snssd ⊢ φ → ∑ G F ⊆ B
15 toponuni ⊢ TopOpen ⁡ G ∈ TopOn ⁡ B → B = ⋃ TopOpen ⁡ G
16 10 15 syl ⊢ φ → B = ⋃ TopOpen ⁡ G
17 14 16 sseqtrd ⊢ φ → ∑ G F ⊆ ⋃ TopOpen ⁡ G
18 eqid ⊢ ⋃ TopOpen ⁡ G = ⋃ TopOpen ⁡ G
19 18 sscls ⊢ TopOpen ⁡ G ∈ Top ∧ ∑ G F ⊆ ⋃ TopOpen ⁡ G → ∑ G F ⊆ cls ⁡ TopOpen ⁡ G ⁡ ∑ G F
20 12 17 19 syl2anc ⊢ φ → ∑ G F ⊆ cls ⁡ TopOpen ⁡ G ⁡ ∑ G F
21 ovex ⊢ ∑ G F ∈ V
22 21 snss ⊢ ∑ G F ∈ cls ⁡ TopOpen ⁡ G ⁡ ∑ G F ↔ ∑ G F ⊆ cls ⁡ TopOpen ⁡ G ⁡ ∑ G F
23 20 22 sylibr ⊢ φ → ∑ G F ∈ cls ⁡ TopOpen ⁡ G ⁡ ∑ G F
24 1 2 3 4 5 6 7 8 tsmsgsum ⊢ φ → G tsums F = cls ⁡ TopOpen ⁡ G ⁡ ∑ G F
25 23 24 eleqtrrd ⊢ φ → ∑ G F ∈ G tsums F