Metamath Proof Explorer


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 ) ) )