Theorem tsmsval

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tsmsval.b	$$⊢B={\mathrm{Base}}_G$$
	tsmsval.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
	tsmsval.s	$$⊢S=𝒫A\cap \mathrm{Fin}$$
	tsmsval.l	$$⊢L=\mathrm{ran}\left(z\in S⟼\left\{y\in S|z\subseteq y\right\}\right)$$
	tsmsval.g	$$⊢\phi \to G\in V$$
	tsmsval.a	$$⊢\phi \to A\in W$$
	tsmsval.f	$$⊢\phi \to F:A⟶B$$
Assertion	tsmsval	$$⊢\phi \to G\mathrm{tsums}F=\left(J\mathrm{fLimf}\left(S\mathrm{filGen}L\right)\right)\left(\left(y\in S⟼{\sum }_G\left({F\upharpoonright }_y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tsmsval.b	$$⊢B={\mathrm{Base}}_G$$
2		tsmsval.j	$$⊢J=\mathrm{TopOpen}\left(G\right)$$
3		tsmsval.s	$$⊢S=𝒫A\cap \mathrm{Fin}$$
4		tsmsval.l	$$⊢L=\mathrm{ran}\left(z\in S⟼\left\{y\in S|z\subseteq y\right\}\right)$$
5		tsmsval.g	$$⊢\phi \to G\in V$$
6		tsmsval.a	$$⊢\phi \to A\in W$$
7		tsmsval.f	$$⊢\phi \to F:A⟶B$$
8	1	fvexi	$$⊢B\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to B\in \mathrm{V}$$
10		fex2	$$⊢\left(F:A⟶B\wedge A\in W\wedge B\in \mathrm{V}\right)\to F\in \mathrm{V}$$
11	7 6 9 10	syl3anc	$$⊢\phi \to F\in \mathrm{V}$$
12	7	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
13	1 2 3 4 5 11 12	tsmsval2	$$⊢\phi \to G\mathrm{tsums}F=\left(J\mathrm{fLimf}\left(S\mathrm{filGen}L\right)\right)\left(\left(y\in S⟼{\sum }_G\left({F\upharpoonright }_y\right)\right)\right)$$