gsummptfidmsplit

Description: Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfidmsplit.b	$⊢ B = {Base}_{G}$
	gsummptfidmsplit.p	$⊢ \underset{˙}{+} = +_{G}$
	gsummptfidmsplit.g	$⊢ φ \to G \in CMnd$
	gsummptfidmsplit.a	$⊢ φ \to A \in Fin$
	gsummptfidmsplit.y	$⊢ (φ \land k \in A) \to Y \in B$
	gsummptfidmsplit.i	$⊢ φ \to C \cap D = \emptyset$
	gsummptfidmsplit.u	$⊢ φ \to A = C \cup D$
Assertion	gsummptfidmsplit	$⊢ φ \to \underset{k \in A}{\sum_{G}} Y = (\underset{k \in C}{\sum_{G}}, Y) \underset{˙}{+} (\underset{k \in D}{\sum_{G}}, Y)$

Step	Hyp	Ref	Expression
1		gsummptfidmsplit.b	$⊢ B = {Base}_{G}$
2		gsummptfidmsplit.p	$⊢ \underset{˙}{+} = +_{G}$
3		gsummptfidmsplit.g	$⊢ φ \to G \in CMnd$
4		gsummptfidmsplit.a	$⊢ φ \to A \in Fin$
5		gsummptfidmsplit.y	$⊢ (φ \land k \in A) \to Y \in B$
6		gsummptfidmsplit.i	$⊢ φ \to C \cap D = \emptyset$
7		gsummptfidmsplit.u	$⊢ φ \to A = C \cup D$
8		eqid	$⊢ 0_{G} = 0_{G}$
9		eqid	$⊢ (k \in A ⟼ Y) = (k \in A ⟼ Y)$
10		fvexd	$⊢ φ \to 0_{G} \in V$
11	9 4 5 10	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} ((k \in A ⟼ Y))$
12	1 8 2 3 4 5 11 6 7	gsumsplit2	$⊢ φ \to \underset{k \in A}{\sum_{G}} Y = (\underset{k \in C}{\sum_{G}}, Y) \underset{˙}{+} (\underset{k \in D}{\sum_{G}}, Y)$

Metamath Proof Explorer