Theorem tsmslem1

Description: The finite partial sums of a function F are defined in a commutative monoid. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tsmslem1.b	$$⊢B={\mathrm{Base}}_G$$
	tsmslem1.s	$$⊢S=𝒫A\cap \mathrm{Fin}$$
	tsmslem1.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
	tsmslem1.a	$$⊢\phi \to A\in W$$
	tsmslem1.f	$$⊢\phi \to F:A⟶B$$
Assertion	tsmslem1	$$⊢\left(\phi \wedge X\in S\right)\to {\sum }_G\left({F\upharpoonright }_X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		tsmslem1.b	$$⊢B={\mathrm{Base}}_G$$
2		tsmslem1.s	$$⊢S=𝒫A\cap \mathrm{Fin}$$
3		tsmslem1.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		tsmslem1.a	$$⊢\phi \to A\in W$$
5		tsmslem1.f	$$⊢\phi \to F:A⟶B$$
6		eqid	$$⊢0_G=0_G$$
7	3	adantr	$$⊢\left(\phi \wedge X\in S\right)\to G\in \mathrm{CMnd}$$
8		simpr	$$⊢\left(\phi \wedge X\in S\right)\to X\in S$$
9	5	adantr	$$⊢\left(\phi \wedge X\in S\right)\to F:A⟶B$$
10	8 2	eleqtrdi	$$⊢\left(\phi \wedge X\in S\right)\to X\in \left(𝒫A\cap \mathrm{Fin}\right)$$
11		elfpw	$$⊢X\in \left(𝒫A\cap \mathrm{Fin}\right)\leftrightarrow \left(X\subseteq A\wedge X\in \mathrm{Fin}\right)$$
12	11	simplbi	$$⊢X\in \left(𝒫A\cap \mathrm{Fin}\right)\to X\subseteq A$$
13	10 12	syl	$$⊢\left(\phi \wedge X\in S\right)\to X\subseteq A$$
14	9 13	fssresd	$$⊢\left(\phi \wedge X\in S\right)\to \left({F\upharpoonright }_X\right):X⟶B$$
15	10	elin2d	$$⊢\left(\phi \wedge X\in S\right)\to X\in \mathrm{Fin}$$
16		fvexd	$$⊢\left(\phi \wedge X\in S\right)\to 0_G\in \mathrm{V}$$
17	14 15 16	fdmfifsupp	$$⊢\left(\phi \wedge X\in S\right)\to {finSupp}_{0_G}\left(\left({F\upharpoonright }_X\right)\right)$$
18	1 6 7 8 14 17	gsumcl	$$⊢\left(\phi \wedge X\in S\right)\to {\sum }_G\left({F\upharpoonright }_X\right)\in B$$