Theorem tsmscl

Description: A sum in a topological group is an element of the group. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tsmscl.b	$$⊢B={\mathrm{Base}}_G$$
	tsmscl.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
	tsmscl.2	$$⊢\phi \to G\in \mathrm{TopSp}$$
	tsmscl.a	$$⊢\phi \to A\in V$$
	tsmscl.f	$$⊢\phi \to F:A⟶B$$
Assertion	tsmscl	$$⊢\phi \to G\mathrm{tsums}F\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		tsmscl.b	$$⊢B={\mathrm{Base}}_G$$
2		tsmscl.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
3		tsmscl.2	$$⊢\phi \to G\in \mathrm{TopSp}$$
4		tsmscl.a	$$⊢\phi \to A\in V$$
5		tsmscl.f	$$⊢\phi \to F:A⟶B$$
6		eqid	$$⊢\mathrm{TopOpen}\left(G\right)=\mathrm{TopOpen}\left(G\right)$$
7		eqid	$$⊢𝒫A\cap \mathrm{Fin}=𝒫A\cap \mathrm{Fin}$$
8	1 6 7 2 3 4 5	eltsms	$$⊢\phi \to \left(x\in \left(G\mathrm{tsums}F\right)\leftrightarrow \left(x\in B\wedge \forall w\in \mathrm{TopOpen}\left(G\right)\left(x\in w\to \exists z\in \left(𝒫A\cap \mathrm{Fin}\right)\forall y\in \left(𝒫A\cap \mathrm{Fin}\right)\left(z\subseteq y\to {\sum }_G\left({F\upharpoonright }_y\right)\in w\right)\right)\right)\right)$$
9		simpl	$$⊢\left(x\in B\wedge \forall w\in \mathrm{TopOpen}\left(G\right)\left(x\in w\to \exists z\in \left(𝒫A\cap \mathrm{Fin}\right)\forall y\in \left(𝒫A\cap \mathrm{Fin}\right)\left(z\subseteq y\to {\sum }_G\left({F\upharpoonright }_y\right)\in w\right)\right)\right)\to x\in B$$
10	8 9	syl6bi	$$⊢\phi \to \left(x\in \left(G\mathrm{tsums}F\right)\to x\in B\right)$$
11	10	ssrdv	$$⊢\phi \to G\mathrm{tsums}F\subseteq B$$