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 = ( Base ` G )
	tsmslem1.s	|- S = ( ~P A i^i Fin )
	tsmslem1.1	|- ( ph -> G e. CMnd )
	tsmslem1.a	|- ( ph -> A e. W )
	tsmslem1.f	|- ( ph -> F : A --> B )
Assertion	tsmslem1	|- ( ( ph /\ X e. S ) -> ( G gsum ( F |` X ) ) e. B )

Proof

Step	Hyp	Ref	Expression
1		tsmslem1.b	|- B = ( Base ` G )
2		tsmslem1.s	|- S = ( ~P A i^i Fin )
3		tsmslem1.1	|- ( ph -> G e. CMnd )
4		tsmslem1.a	|- ( ph -> A e. W )
5		tsmslem1.f	|- ( ph -> F : A --> B )
6		eqid	|- ( 0g ` G ) = ( 0g ` G )
7	3	adantr	|- ( ( ph /\ X e. S ) -> G e. CMnd )
8		simpr	|- ( ( ph /\ X e. S ) -> X e. S )
9	5	adantr	|- ( ( ph /\ X e. S ) -> F : A --> B )
10	8 2	eleqtrdi	|- ( ( ph /\ X e. S ) -> X e. ( ~P A i^i Fin ) )
11		elfpw	|- ( X e. ( ~P A i^i Fin ) <-> ( X C_ A /\ X e. Fin ) )
12	11	simplbi	|- ( X e. ( ~P A i^i Fin ) -> X C_ A )
13	10 12	syl	|- ( ( ph /\ X e. S ) -> X C_ A )
14	9 13	fssresd	|- ( ( ph /\ X e. S ) -> ( F |` X ) : X --> B )
15	10	elin2d	|- ( ( ph /\ X e. S ) -> X e. Fin )
16		fvexd	|- ( ( ph /\ X e. S ) -> ( 0g ` G ) e. _V )
17	14 15 16	fdmfifsupp	|- ( ( ph /\ X e. S ) -> ( F |` X ) finSupp ( 0g ` G ) )
18	1 6 7 8 14 17	gsumcl	|- ( ( ph /\ X e. S ) -> ( G gsum ( F |` X ) ) e. B )