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 𝐹 ) )