gsumsplit

Description: Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 5-Jun-2019)

	Ref	Expression
Hypotheses	gsumsplit.b	$⊢ B = {Base}_{G}$
	gsumsplit.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumsplit.p	$⊢ \underset{˙}{+} = +_{G}$
	gsumsplit.g	$⊢ φ \to G \in CMnd$
	gsumsplit.a	$⊢ φ \to A \in V$
	gsumsplit.f	$⊢ φ \to F : A ⟶ B$
	gsumsplit.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
	gsumsplit.i	$⊢ φ \to C \cap D = \emptyset$
	gsumsplit.u	$⊢ φ \to A = C \cup D$
Assertion	gsumsplit	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D}))$

Step	Hyp	Ref	Expression
1		gsumsplit.b	$⊢ B = {Base}_{G}$
2		gsumsplit.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumsplit.p	$⊢ \underset{˙}{+} = +_{G}$
4		gsumsplit.g	$⊢ φ \to G \in CMnd$
5		gsumsplit.a	$⊢ φ \to A \in V$
6		gsumsplit.f	$⊢ φ \to F : A ⟶ B$
7		gsumsplit.w	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
8		gsumsplit.i	$⊢ φ \to C \cap D = \emptyset$
9		gsumsplit.u	$⊢ φ \to A = C \cup D$
10		eqid	$⊢ Cntz (G) = Cntz (G)$
11		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
12	4 11	syl	$⊢ φ \to G \in Mnd$
13	1 10 4 6	cntzcmnf	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
14	1 2 3 10 12 5 6 13 7 8 9	gsumzsplit	$⊢ φ \to \sum_{G} F = (\sum_{G}, ({F ↾}_{C})) \underset{˙}{+} (\sum_{G}, ({F ↾}_{D}))$

Metamath Proof Explorer