tsmslem1

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

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

Metamath Proof Explorer