Theorem haustsmsid

Description: In a Hausdorff topological group, a finite sum sums to exactly the usual number with no extraneous limit points. By setting the topology to the discrete topology (which is Hausdorff), this theorem can be used to turn any tsums theorem into a gsum theorem, so that the infinite group sum operation can be viewed as a generalization of the finite group sum. (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 )
	haustsmsid.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	haustsmsid.h	⊢ ( 𝜑 → 𝐽 ∈ Haus )
Assertion	haustsmsid	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = { ( 𝐺 Σg 𝐹 ) } )

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		haustsmsid.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
9		haustsmsid.h	⊢ ( 𝜑 → 𝐽 ∈ Haus )
10	1 2 3 4 5 6 7	tsmsid	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) )
11	1 3 4 5 6 8 9	haustsms2	⊢ ( 𝜑 → ( ( 𝐺 Σg 𝐹 ) ∈ ( 𝐺 tsums 𝐹 ) → ( 𝐺 tsums 𝐹 ) = { ( 𝐺 Σg 𝐹 ) } ) )
12	10 11	mpd	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = { ( 𝐺 Σg 𝐹 ) } )