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

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsid.z ⊢ 0 = ( 0g ‘ 𝐺 )
tsmsid.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmsid.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmsid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmsid.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmsid.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion tsmsid ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tsmsid.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmsid.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 tsmsid.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 tsmsid.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
5 tsmsid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 tsmsid.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 tsmsid.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
8 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
9 1 8 istps ⊢ ( 𝐺 ∈ TopSp ↔ ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
10 4 9 sylib ⊢ ( 𝜑 → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
11 topontop ⊢ ( ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) → ( TopOpen ‘ 𝐺 ) ∈ Top )
12 10 11 syl ⊢ ( 𝜑 → ( TopOpen ‘ 𝐺 ) ∈ Top )
13 1 2 3 5 6 7 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ 𝐵 )
14 13 snssd ⊢ ( 𝜑 → { ( 𝐺 Σg 𝐹 ) } ⊆ 𝐵 )
15 toponuni ⊢ ( ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = ∪ ( TopOpen ‘ 𝐺 ) )
16 10 15 syl ⊢ ( 𝜑 → 𝐵 = ∪ ( TopOpen ‘ 𝐺 ) )
17 14 16 sseqtrd ⊢ ( 𝜑 → { ( 𝐺 Σg 𝐹 ) } ⊆ ∪ ( TopOpen ‘ 𝐺 ) )
18 eqid ⊢ ∪ ( TopOpen ‘ 𝐺 ) = ∪ ( TopOpen ‘ 𝐺 )
19 18 sscls ⊢ ( ( ( TopOpen ‘ 𝐺 ) ∈ Top ∧ { ( 𝐺 Σg 𝐹 ) } ⊆ ∪ ( TopOpen ‘ 𝐺 ) ) → { ( 𝐺 Σg 𝐹 ) } ⊆ ( ( cls ‘ ( TopOpen ‘ 𝐺 ) ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )
20 12 17 19 syl2anc ⊢ ( 𝜑 → { ( 𝐺 Σg 𝐹 ) } ⊆ ( ( cls ‘ ( TopOpen ‘ 𝐺 ) ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )
21 ovex ⊢ ( 𝐺 Σg 𝐹 ) ∈ V
22 21 snss ⊢ ( ( 𝐺 Σg 𝐹 ) ∈ ( ( cls ‘ ( TopOpen ‘ 𝐺 ) ) ‘ { ( 𝐺 Σg 𝐹 ) } ) ↔ { ( 𝐺 Σg 𝐹 ) } ⊆ ( ( cls ‘ ( TopOpen ‘ 𝐺 ) ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )
23 20 22 sylibr ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( ( cls ‘ ( TopOpen ‘ 𝐺 ) ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )
24 1 2 3 4 5 6 7 8 tsmsgsum ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( cls ‘ ( TopOpen ‘ 𝐺 ) ) ‘ { ( 𝐺 Σg 𝐹 ) } ) )
25 23 24 eleqtrrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) )