gsumcom3

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

	Ref	Expression
Hypotheses	gsumcom3.b	$⊢ B = {Base}_{G}$
	gsumcom3.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumcom3.g	$⊢ φ \to G \in CMnd$
	gsumcom3.a	$⊢ φ \to A \in V$
	gsumcom3.r	$⊢ φ \to C \in W$
	gsumcom3.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
	gsumcom3.u	$⊢ φ \to U \in Fin$
	gsumcom3.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
Assertion	gsumcom3	$⊢ φ \to \underset{j \in A}{\sum_{G}} (\underset{k \in C}{\sum_{G}}, X) = \underset{k \in C}{\sum_{G}} (\underset{j \in A}{\sum_{G}}, X)$

Proof

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

Metamath Proof Explorer

Theorem gsumcom3

Proof