Theorem gsumcom3

Description: A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015)

	Ref	Expression
Hypotheses	gsumcom3.b	$$⊢B={\mathrm{Base}}_G$$
	gsumcom3.z	$$⊢\underset{\dot{}}{0}=0_G$$
	gsumcom3.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
	gsumcom3.a	$$⊢\phi \to A\in V$$
	gsumcom3.r	$$⊢\phi \to C\in W$$
	gsumcom3.f	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in C\right)\right)\to X\in B$$
	gsumcom3.u	$$⊢\phi \to U\in \mathrm{Fin}$$
	gsumcom3.n	$$⊢\left(\phi \wedge \left(\left(j\in A\wedge k\in C\right)\wedge \neg jUk\right)\right)\to X=\underset{\dot{}}{0}$$
Assertion	gsumcom3	$$⊢\phi \to \underset{j\in A}{{\sum }_G}\left(\underset{k\in C}{{\sum }_G},X\right)=\underset{k\in C}{{\sum }_G}\left(\underset{j\in A}{{\sum }_G},X\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumcom3.b	$$⊢B={\mathrm{Base}}_G$$
2		gsumcom3.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		gsumcom3.g	$$⊢\phi \to G\in \mathrm{CMnd}$$
4		gsumcom3.a	$$⊢\phi \to A\in V$$
5		gsumcom3.r	$$⊢\phi \to C\in W$$
6		gsumcom3.f	$$⊢\left(\phi \wedge \left(j\in A\wedge k\in C\right)\right)\to X\in B$$
7		gsumcom3.u	$$⊢\phi \to U\in \mathrm{Fin}$$
8		gsumcom3.n	$$⊢\left(\phi \wedge \left(\left(j\in A\wedge k\in C\right)\wedge \neg jUk\right)\right)\to X=\underset{\dot{}}{0}$$
9	1 2 3 4 5 6 7 8	gsumcom	$$⊢\phi \to {\sum }_G\left(j\in A,k\in C⟼X\right)={\sum }_G\left(k\in C,j\in A⟼X\right)$$
10	5	adantr	$$⊢\left(\phi \wedge j\in A\right)\to C\in W$$
11	1 2 3 4 10 6 7 8	gsum2d2	$$⊢\phi \to {\sum }_G\left(j\in A,k\in C⟼X\right)=\underset{j\in A}{{\sum }_G}\left(\underset{k\in C}{{\sum }_G},X\right)$$
12	4	adantr	$$⊢\left(\phi \wedge k\in C\right)\to A\in V$$
13	6	ancom2s	$$⊢\left(\phi \wedge \left(k\in C\wedge j\in A\right)\right)\to X\in B$$
14		cnvfi	$$⊢U\in \mathrm{Fin}\to U^{-1}\in \mathrm{Fin}$$
15	7 14	syl	$$⊢\phi \to U^{-1}\in \mathrm{Fin}$$
16		ancom	$$⊢\left(k\in C\wedge j\in A\right)\leftrightarrow \left(j\in A\wedge k\in C\right)$$
17		vex	$$⊢k\in \mathrm{V}$$
18		vex	$$⊢j\in \mathrm{V}$$
19	17 18	brcnv	$$⊢k{U}^{-1}j\leftrightarrow jUk$$
20	19	notbii	$$⊢\neg k{U}^{-1}j\leftrightarrow \neg jUk$$
21	16 20	anbi12i	$$⊢\left(\left(k\in C\wedge j\in A\right)\wedge \neg k{U}^{-1}j\right)\leftrightarrow \left(\left(j\in A\wedge k\in C\right)\wedge \neg jUk\right)$$
22	21 8	sylan2b	$$⊢\left(\phi \wedge \left(\left(k\in C\wedge j\in A\right)\wedge \neg k{U}^{-1}j\right)\right)\to X=\underset{\dot{}}{0}$$
23	1 2 3 5 12 13 15 22	gsum2d2	$$⊢\phi \to {\sum }_G\left(k\in C,j\in A⟼X\right)=\underset{k\in C}{{\sum }_G}\left(\underset{j\in A}{{\sum }_G},X\right)$$
24	9 11 23	3eqtr3d	$$⊢\phi \to \underset{j\in A}{{\sum }_G}\left(\underset{k\in C}{{\sum }_G},X\right)=\underset{k\in C}{{\sum }_G}\left(\underset{j\in A}{{\sum }_G},X\right)$$