gsumcom3fi

Description: A commutative law for finite iterated sums. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	gsumcom3fi.b	$⊢ B = {Base}_{G}$
	gsumcom3fi.g	$⊢ φ \to G \in CMnd$
	gsumcom3fi.a	$⊢ φ \to A \in Fin$
	gsumcom3fi.r	$⊢ φ \to C \in Fin$
	gsumcom3fi.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
Assertion	gsumcom3fi	$⊢ φ \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)$

Step	Hyp	Ref	Expression
1		gsumcom3fi.b	$⊢ B = {Base}_{G}$
2		gsumcom3fi.g	$⊢ φ \to G \in CMnd$
3		gsumcom3fi.a	$⊢ φ \to A \in Fin$
4		gsumcom3fi.r	$⊢ φ \to C \in Fin$
5		gsumcom3fi.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
6		eqid	$⊢ 0_{G} = 0_{G}$
7		xpfi	$⊢ (A \in Fin \land C \in Fin) \to A \times C \in Fin$
8	3 4 7	syl2anc	$⊢ φ \to A \times C \in Fin$
9		brxp	$⊢ j (A \times C) k \leftrightarrow (j \in A \land k \in C)$
10	9	bilanri	$⊢ (φ \land (j \in A \land k \in C)) \to j (A \times C) k$
11	10	pm2.24d	$⊢ (φ \land (j \in A \land k \in C)) \to (\neg j (A \times C) k \to X = 0_{G})$
12	11	impr	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j (A \times C) k)) \to X = 0_{G}$
13	1 6 2 3 4 5 8 12	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)$

Metamath Proof Explorer