gsummptfidmsplitres

Description: Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (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$
	gsummptfidmsplitres.f	$⊢ F = (k \in A ⟼ Y)$
Assertion	gsummptfidmsplitres	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D}))$

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		gsummptfidmsplitres.f	$⊢ F = (k \in A ⟼ Y)$
9		eqid	$⊢ 0_{G} = 0_{G}$
10	5 8	fmptd	$⊢ φ \to F : A ⟶ B$
11		fvexd	$⊢ φ \to 0_{G} \in V$
12	8 4 5 11	fsuppmptdm	$⊢ φ \to {finSupp}_{0_{G}} (F)$
13	1 9 2 3 4 10 12 6 7	gsumsplit	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D}))$

Metamath Proof Explorer