Theorem gsumcom

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

	Ref	Expression
Hypotheses	gsumxp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumxp.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumxp.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumxp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumxp.r	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
	gsumcom.f	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 )
	gsumcom.u	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	gsumcom.n	⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
Assertion	gsumcom	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 , 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumxp.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumxp.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumxp.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsumxp.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		gsumxp.r	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		gsumcom.f	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 )
7		gsumcom.u	⊢ ( 𝜑 → 𝑈 ∈ Fin )
8		gsumcom.n	⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
9	5	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
10		ancom	⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) )
11	10	a1i	⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐴 ) ) )
12	1 2 3 4 9 6 7 8 5 11	gsumcom2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 , 𝑗 ∈ 𝐴 ↦ 𝑋 ) ) )