gsumcom

Description: Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014)

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

Step	Hyp	Ref	Expression
1		gsumxp.b	$⊢ B = {Base}_{G}$
2		gsumxp.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumxp.g	$⊢ φ \to G \in CMnd$
4		gsumxp.a	$⊢ φ \to A \in V$
5		gsumxp.r	$⊢ φ \to C \in W$
6		gsumcom.f	$⊢ (φ \land (j \in A \land k \in C)) \to X \in B$
7		gsumcom.u	$⊢ φ \to U \in Fin$
8		gsumcom.n	$⊢ (φ \land ((j \in A \land k \in C) \land \neg j U k)) \to X = \underset{˙}{0}$
9	5	adantr	$⊢ (φ \land j \in A) \to C \in W$
10		ancom	$⊢ (j \in A \land k \in C) \leftrightarrow (k \in C \land j \in A)$
11	10	a1i	$⊢ φ \to ((j \in A \land k \in C) \leftrightarrow (k \in C \land j \in A))$
12	1 2 3 4 9 6 7 8 5 11	gsumcom2	$⊢ φ \to \sum_{G} (j \in A, k \in C ⟼ X) = \sum_{G} (k \in C, j \in A ⟼ X)$

Metamath Proof Explorer