Theorem 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	|- ( ph -> G e. CMnd )
	gsumcom3fi.a	|- ( ph -> A e. Fin )
	gsumcom3fi.r	|- ( ph -> C e. Fin )
	gsumcom3fi.f	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
Assertion	gsumcom3fi	|- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumcom3fi.b	|- B = ( Base ` G )
2		gsumcom3fi.g	|- ( ph -> G e. CMnd )
3		gsumcom3fi.a	|- ( ph -> A e. Fin )
4		gsumcom3fi.r	|- ( ph -> C e. Fin )
5		gsumcom3fi.f	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> X e. B )
6		eqid	|- ( 0g ` G ) = ( 0g ` G )
7		xpfi	|- ( ( A e. Fin /\ C e. Fin ) -> ( A X. C ) e. Fin )
8	3 4 7	syl2anc	|- ( ph -> ( A X. C ) e. Fin )
9		brxp	|- ( j ( A X. C ) k <-> ( j e. A /\ k e. C ) )
10	9	biimpri	|- ( ( j e. A /\ k e. C ) -> j ( A X. C ) k )
11	10	adantl	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> j ( A X. C ) k )
12	11	pm2.24d	|- ( ( ph /\ ( j e. A /\ k e. C ) ) -> ( -. j ( A X. C ) k -> X = ( 0g ` G ) ) )
13	12	impr	|- ( ( ph /\ ( ( j e. A /\ k e. C ) /\ -. j ( A X. C ) k ) ) -> X = ( 0g ` G ) )
14	1 6 2 3 4 5 8 13	gsumcom3	|- ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> X ) ) ) ) = ( G gsum ( k e. C |-> ( G gsum ( j e. A |-> X ) ) ) ) )