Theorem 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={\mathrm{Base}}_G$$
	gsumsplit.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumsplit.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumsplit.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumsplit.a	$$⊢\phi \to A\in V$$
	gsumsplit.f	$$⊢\phi \to F:A⟶B$$
	gsumsplit.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
	gsumsplit.i	$$⊢\phi \to C\cap D=\varnothing$$
	gsumsplit.u	$$⊢\phi \to A=C\cup D$$
Assertion	gsumsplit	$$⊢\phi \to {\sum }_{G}F=\left({\sum }_G,\left({F\upharpoonright }_C\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({F\upharpoonright }_D\right)\right)$$

Proof

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