Theorem gsumxp

Description: Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Hypotheses	gsumxp.b	$$⊢B={\mathrm{Base}}_G$$
	gsumxp.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumxp.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumxp.a	$$⊢\phi \to A\in V$$
	gsumxp.r	$$⊢\phi \to C\in W$$
	gsumxp.f	$$⊢\phi \to F:A\times C⟶B$$
	gsumxp.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	gsumxp	$$⊢\phi \to {\sum }_{G}F=\underset{j\in A}{{\sum }_G}\left(\underset{k\in C}{{\sum }_G},\left(jFk\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumxp.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumxp.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumxp.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumxp.a	$$⊢\phi \to A\in V$$
5		gsumxp.r	$$⊢\phi \to C\in W$$
6		gsumxp.f	$$⊢\phi \to F:A\times C⟶B$$
7		gsumxp.w	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
8	4 5	xpexd	$$⊢\phi \to A\times C\in \mathrm{V}$$
9		relxp	$$⊢\mathrm{Rel}\left(A\times C\right)$$
10	9	a1i	$$⊢\phi \to \mathrm{Rel}\left(A\times C\right)$$
11		dmxpss	$$⊢\mathrm{dom}\left(A\times C\right)\subseteq A$$
12	11	a1i	$$⊢\phi \to \mathrm{dom}\left(A\times C\right)\subseteq A$$
13	1 2 3 8 10 4 12 6 7	gsum2d	$$⊢\phi \to {\sum }_{G}F=\underset{j\in A}{{\sum }_G}\left(\underset{k\in \left(A\times C\right)\left[\left\{j\right\}\right]}{{\sum }_G},\left(jFk\right)\right)$$
14		df-ima	$$⊢\left(A\times C\right)\left[\left\{j\right\}\right]=\mathrm{ran}\left({\left(A\times C\right)\upharpoonright }_{\left\{j\right\}}\right)$$
15		df-res	$$⊢{\left(A\times C\right)\upharpoonright }_{\left\{j\right\}}=\left(A\times C\right)\cap \left(\left\{j\right\}\times \mathrm{V}\right)$$
16		inxp	$$⊢\left(A\times C\right)\cap \left(\left\{j\right\}\times \mathrm{V}\right)=\left(A\cap \left\{j\right\}\right)\times \left(C\cap \mathrm{V}\right)$$
17	15 16	eqtri	$$⊢{\left(A\times C\right)\upharpoonright }_{\left\{j\right\}}=\left(A\cap \left\{j\right\}\right)\times \left(C\cap \mathrm{V}\right)$$
18		simpr	$$⊢\left(\phi \wedge j\in A\right)\to j\in A$$
19	18	snssd	$$⊢\left(\phi \wedge j\in A\right)\to \left\{j\right\}\subseteq A$$
20		sseqin2	$$⊢\left\{j\right\}\subseteq A\leftrightarrow A\cap \left\{j\right\}=\left\{j\right\}$$
21	19 20	sylib	$$⊢\left(\phi \wedge j\in A\right)\to A\cap \left\{j\right\}=\left\{j\right\}$$
22		inv1	$$⊢C\cap \mathrm{V}=C$$
23	22	a1i	$$⊢\left(\phi \wedge j\in A\right)\to C\cap \mathrm{V}=C$$
24	21 23	xpeq12d	$$⊢\left(\phi \wedge j\in A\right)\to \left(A\cap \left\{j\right\}\right)\times \left(C\cap \mathrm{V}\right)=\left\{j\right\}\times C$$
25	17 24	eqtrid	$$⊢\left(\phi \wedge j\in A\right)\to {\left(A\times C\right)\upharpoonright }_{\left\{j\right\}}=\left\{j\right\}\times C$$
26	25	rneqd	$$⊢\left(\phi \wedge j\in A\right)\to \mathrm{ran}\left({\left(A\times C\right)\upharpoonright }_{\left\{j\right\}}\right)=\mathrm{ran}\left(\left\{j\right\}\times C\right)$$
27		vex	$$⊢j\in \mathrm{V}$$
28	27	snnz	$$⊢\left\{j\right\}\ne \varnothing$$
29		rnxp	$$⊢\left\{j\right\}\ne \varnothing \to \mathrm{ran}\left(\left\{j\right\}\times C\right)=C$$
30	28 29	ax-mp	$$⊢\mathrm{ran}\left(\left\{j\right\}\times C\right)=C$$
31	26 30	eqtrdi	$$⊢\left(\phi \wedge j\in A\right)\to \mathrm{ran}\left({\left(A\times C\right)\upharpoonright }_{\left\{j\right\}}\right)=C$$
32	14 31	eqtrid	$$⊢\left(\phi \wedge j\in A\right)\to \left(A\times C\right)\left[\left\{j\right\}\right]=C$$
33	32	mpteq1d	$$⊢\left(\phi \wedge j\in A\right)\to \left(k\in \left(A\times C\right)\left[\left\{j\right\}\right]⟼jFk\right)=\left(k\in C⟼jFk\right)$$
34	33	oveq2d	$$⊢\left(\phi \wedge j\in A\right)\to \underset{k\in \left(A\times C\right)\left[\left\{j\right\}\right]}{{\sum }_G}\left(jFk\right)=\underset{k\in C}{{\sum }_G}\left(jFk\right)$$
35	34	mpteq2dva	$$⊢\phi \to \left(j\in A⟼\underset{k\in \left(A\times C\right)\left[\left\{j\right\}\right]}{{\sum }_G}\left(jFk\right)\right)=\left(j\in A⟼\underset{k\in C}{{\sum }_G}\left(jFk\right)\right)$$
36	35	oveq2d	$$⊢\phi \to \underset{j\in A}{{\sum }_G}\left(\underset{k\in \left(A\times C\right)\left[\left\{j\right\}\right]}{{\sum }_G},\left(jFk\right)\right)=\underset{j\in A}{{\sum }_G}\left(\underset{k\in C}{{\sum }_G},\left(jFk\right)\right)$$
37	13 36	eqtrd	$$⊢\phi \to {\sum }_{G}F=\underset{j\in A}{{\sum }_G}\left(\underset{k\in C}{{\sum }_G},\left(jFk\right)\right)$$