Theorem gsumsplit2

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

	Ref	Expression
Hypotheses	gsumsplit2.b	$$⊢B={\mathrm{Base}}_G$$
	gsumsplit2.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumsplit2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	gsumsplit2.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumsplit2.a	$$⊢\phi \to A\in V$$
	gsumsplit2.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
	gsumsplit2.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
	gsumsplit2.i	$$⊢\phi \to C\cap D=\varnothing$$
	gsumsplit2.u	$$⊢\phi \to A=C\cup D$$
Assertion	gsumsplit2	$$⊢\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		gsumsplit2.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumsplit2.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumsplit2.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		gsumsplit2.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
5		gsumsplit2.a	$$⊢\phi \to A\in V$$
6		gsumsplit2.f	$$⊢\left(\phi \wedge k\in A\right)\to X\in B$$
7		gsumsplit2.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in A⟼X\right)\right)$$
8		gsumsplit2.i	$$⊢\phi \to C\cap D=\varnothing$$
9		gsumsplit2.u	$$⊢\phi \to A=C\cup D$$
10	6	fmpttd	$$⊢\phi \to \left(k\in A⟼X\right):A⟶B$$
11	1 2 3 4 5 10 7 8 9	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)$$
12		ssun1	$$⊢C\subseteq C\cup D$$
13	12 9	sseqtrrid	$$⊢\phi \to C\subseteq A$$
14	13	resmptd	$$⊢\phi \to {\left(k\in A⟼X\right)\upharpoonright }_C=\left(k\in C⟼X\right)$$
15	14	oveq2d	$$⊢\phi \to {\sum }_G\left({\left(k\in A⟼X\right)\upharpoonright }_C\right)=\underset{k\in C}{{\sum }_G}X$$
16		ssun2	$$⊢D\subseteq C\cup D$$
17	16 9	sseqtrrid	$$⊢\phi \to D\subseteq A$$
18	17	resmptd	$$⊢\phi \to {\left(k\in A⟼X\right)\upharpoonright }_D=\left(k\in D⟼X\right)$$
19	18	oveq2d	$$⊢\phi \to {\sum }_G\left({\left(k\in A⟼X\right)\upharpoonright }_D\right)=\underset{k\in D}{{\sum }_G}X$$
20	15 19	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)$$
21	11 20	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)$$