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