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={\mathrm{Base}}_G$$
	tsmsid.z	$$⊢\underset{\dot{}}{0}=0_G$$
	tsmsid.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
	tsmsid.2	$$⊢\phi \to G\in \mathrm{TopSp}$$
	tsmsid.a	$$⊢\phi \to A\in V$$
	tsmsid.f	$$⊢\phi \to F:A⟶B$$
	tsmsid.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	tsmsid	$$⊢\phi \to {\sum }_{G}F\in \left(G\mathrm{tsums}F\right)$$

Proof

Step	Hyp	Ref	Expression
1		tsmsid.b	$$⊢B={\mathrm{Base}}_G$$
2		tsmsid.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		tsmsid.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		tsmsid.2	$$⊢\phi \to G\in \mathrm{TopSp}$$
5		tsmsid.a	$$⊢\phi \to A\in V$$
6		tsmsid.f	$$⊢\phi \to F:A⟶B$$
7		tsmsid.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
8		eqid	$$⊢\mathrm{TopOpen}\left(G\right)=\mathrm{TopOpen}\left(G\right)$$
9	1 8	istps	$$⊢G\in \mathrm{TopSp}\leftrightarrow \mathrm{TopOpen}\left(G\right)\in \mathrm{TopOn}\left(B\right)$$
10	4 9	sylib	$$⊢\phi \to \mathrm{TopOpen}\left(G\right)\in \mathrm{TopOn}\left(B\right)$$
11		topontop	$$⊢\mathrm{TopOpen}\left(G\right)\in \mathrm{TopOn}\left(B\right)\to \mathrm{TopOpen}\left(G\right)\in \mathrm{Top}$$
12	10 11	syl	$$⊢\phi \to \mathrm{TopOpen}\left(G\right)\in \mathrm{Top}$$
13	1 2 3 5 6 7	gsumcl	$$⊢\phi \to {\sum }_{G}F\in B$$
14	13	snssd	$$⊢\phi \to \left\{{\sum }_{G}F\right\}\subseteq B$$
15		toponuni	$$⊢\mathrm{TopOpen}\left(G\right)\in \mathrm{TopOn}\left(B\right)\to B=\bigcup \mathrm{TopOpen}\left(G\right)$$
16	10 15	syl	$$⊢\phi \to B=\bigcup \mathrm{TopOpen}\left(G\right)$$
17	14 16	sseqtrd	$$⊢\phi \to \left\{{\sum }_{G}F\right\}\subseteq \bigcup \mathrm{TopOpen}\left(G\right)$$
18		eqid	$$⊢\bigcup \mathrm{TopOpen}\left(G\right)=\bigcup \mathrm{TopOpen}\left(G\right)$$
19	18	sscls	$$⊢\left(\mathrm{TopOpen}\left(G\right)\in \mathrm{Top}\wedge \left\{{\sum }_{G}F\right\}\subseteq \bigcup \mathrm{TopOpen}\left(G\right)\right)\to \left\{{\sum }_{G}F\right\}\subseteq \mathrm{cls}\left(\mathrm{TopOpen}\left(G\right)\right)\left(\left\{{\sum }_{G}F\right\}\right)$$
20	12 17 19	syl2anc	$$⊢\phi \to \left\{{\sum }_{G}F\right\}\subseteq \mathrm{cls}\left(\mathrm{TopOpen}\left(G\right)\right)\left(\left\{{\sum }_{G}F\right\}\right)$$
21		ovex	$$⊢{\sum }_{G}F\in \mathrm{V}$$
22	21	snss	$$⊢{\sum }_{G}F\in \mathrm{cls}\left(\mathrm{TopOpen}\left(G\right)\right)\left(\left\{{\sum }_{G}F\right\}\right)\leftrightarrow \left\{{\sum }_{G}F\right\}\subseteq \mathrm{cls}\left(\mathrm{TopOpen}\left(G\right)\right)\left(\left\{{\sum }_{G}F\right\}\right)$$
23	20 22	sylibr	$$⊢\phi \to {\sum }_{G}F\in \mathrm{cls}\left(\mathrm{TopOpen}\left(G\right)\right)\left(\left\{{\sum }_{G}F\right\}\right)$$
24	1 2 3 4 5 6 7 8	tsmsgsum	$$⊢\phi \to G\mathrm{tsums}F=\mathrm{cls}\left(\mathrm{TopOpen}\left(G\right)\right)\left(\left\{{\sum }_{G}F\right\}\right)$$
25	23 24	eleqtrrd	$$⊢\phi \to {\sum }_{G}F\in \left(G\mathrm{tsums}F\right)$$