Theorem gsumsplit2f

Description: Split a group sum into two parts. (Contributed by AV, 4-Sep-2019)

	Ref	Expression
Hypotheses	gsumsplit2f.n	$$⊢Ⅎk\phi$$
	gsumsplit2f.b	$$⊢B={\mathrm{Base}}_G$$
	gsumsplit2f.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumsplit2f.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumsplit2f.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumsplit2f.a	$$⊢\phi \to A\in V$$
	gsumsplit2f.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumsplit2f.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
	gsumsplit2f.i	$$⊢\phi \to C\cap D=\varnothing$$
	gsumsplit2f.u	$$⊢\phi \to A=C\cup D$$
Assertion	gsumsplit2f	$$⊢\phi \to \underset{k\in A}{{\sum }_G}X=\left(\underset{k\in C}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in D}{{\sum }_G},X\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumsplit2f.n	$$⊢Ⅎk\phi$$
2		gsumsplit2f.b	$$⊢B={\mathrm{Base}}_G$$
3		gsumsplit2f.z	$$⊢\underset{\dot{}}{0}=0_G$$
4		gsumsplit2f.p	$$⊢\underset{\dot{}}{+}={+}_G$$
5		gsumsplit2f.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
6		gsumsplit2f.a	$$⊢\phi \to A\in V$$
7		gsumsplit2f.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
8		gsumsplit2f.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
9		gsumsplit2f.i	$$⊢\phi \to C\cap D=\varnothing$$
10		gsumsplit2f.u	$$⊢\phi \to A=C\cup D$$
11		eqid	$$⊢\left(k\in A⟼X\right)=\left(k\in A⟼X\right)$$
12	1 7 11	fmptdf	$$⊢\phi \to \left(k\in A⟼X\right):A⟶B$$
13	2 3 4 5 6 12 8 9 10	gsumsplit	$$⊢\phi \to \underset{k\in A}{{\sum }_G}X=\left({\sum }_G,\left({\left(k\in A⟼X\right)\upharpoonright }_C\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({\left(k\in A⟼X\right)\upharpoonright }_D\right)\right)$$
14		ssun1	$$⊢C\subseteq C\cup D$$
15	14 10	sseqtrrid	$$⊢\phi \to C\subseteq A$$
16	15	resmptd	$$⊢\phi \to {\left(k\in A⟼X\right)\upharpoonright }_C=\left(k\in C⟼X\right)$$
17	16	oveq2d	$$⊢\phi \to {\sum }_G\left({\left(k\in A⟼X\right)\upharpoonright }_C\right)=\underset{k\in C}{{\sum }_G}X$$
18		ssun2	$$⊢D\subseteq C\cup D$$
19	18 10	sseqtrrid	$$⊢\phi \to D\subseteq A$$
20	19	resmptd	$$⊢\phi \to {\left(k\in A⟼X\right)\upharpoonright }_D=\left(k\in D⟼X\right)$$
21	20	oveq2d	$$⊢\phi \to {\sum }_G\left({\left(k\in A⟼X\right)\upharpoonright }_D\right)=\underset{k\in D}{{\sum }_G}X$$
22	17 21	oveq12d	$$⊢\phi \to \left({\sum }_G,\left({\left(k\in A⟼X\right)\upharpoonright }_C\right)\right)\underset{\dot{}}{+}\left({\sum }_G,\left({\left(k\in A⟼X\right)\upharpoonright }_D\right)\right)=\left(\underset{k\in C}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in D}{{\sum }_G},X\right)$$
23	13 22	eqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }_G}X=\left(\underset{k\in C}{{\sum }_G},X\right)\underset{\dot{}}{+}\left(\underset{k\in D}{{\sum }_G},X\right)$$