Theorem 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	|- .0. = ( 0g ` G )
	gsumxp.g	|- ( ph -> G e. CMnd )
	gsumxp.a	|- ( ph -> A e. V )
	gsumxp.r	|- ( ph -> C e. W )
	gsumcom.f	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
	gsumcom.u	|- ( ph -> U e. Fin )
	gsumcom.n	|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
Assertion	gsumcom	|- ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( k e. C , j e. A |-> X ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumxp.b	|- B = ( Base ` G )
2		gsumxp.z	|- .0. = ( 0g ` G )
3		gsumxp.g	|- ( ph -> G e. CMnd )
4		gsumxp.a	|- ( ph -> A e. V )
5		gsumxp.r	|- ( ph -> C e. W )
6		gsumcom.f	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
7		gsumcom.u	|- ( ph -> U e. Fin )
8		gsumcom.n	|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j U k ) ) -> X = .0. )
9	5	adantr	|- ( ( ph /\ j e. A ) -> C e. W )
10		ancom	|- ( ( j e. A /\ k e. C ) <-> ( k e. C /\ j e. A ) )
11	10	a1i	|- ( ph -> ( ( j e. A /\ k e. C ) <-> ( k e. C /\ j e. A ) ) )
12	1 2 3 4 9 6 7 8 5 11	gsumcom2	|- ( ph -> ( G gsum ( j e. A , k e. C |-> X ) ) = ( G gsum ( k e. C , j e. A |-> X ) ) )