Metamath Proof Explorer

Theorem gsumxp

Description: Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

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 )
gsumxp.f 
|- ( ph -> F : ( A X. C ) --> B )
gsumxp.w 
|- ( ph -> F finSupp .0. )
Assertion gsumxp 
|- ( ph -> ( G gsum F ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) )

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 gsumxp.f 
 |-  ( ph -> F : ( A X. C ) --> B )
7 gsumxp.w 
 |-  ( ph -> F finSupp .0. )
8 4 5 xpexd 
 |-  ( ph -> ( A X. C ) e. _V )
9 relxp 
 |-  Rel ( A X. C )
10 9 a1i 
 |-  ( ph -> Rel ( A X. C ) )
11 dmxpss 
 |-  dom ( A X. C ) C_ A
12 11 a1i 
 |-  ( ph -> dom ( A X. C ) C_ A )
13 1 2 3 8 10 4 12 6 7 gsum2d 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( j e. A |-> ( G gsum ( k e. ( ( A X. C ) " { j } ) |-> ( j F k ) ) ) ) ) )
14 df-ima 
 |-  ( ( A X. C ) " { j } ) = ran ( ( A X. C ) |` { j } )
15 df-res 
 |-  ( ( A X. C ) |` { j } ) = ( ( A X. C ) i^i ( { j } X. _V ) )
16 inxp 
 |-  ( ( A X. C ) i^i ( { j } X. _V ) ) = ( ( A i^i { j } ) X. ( C i^i _V ) )
17 15 16 eqtri 
 |-  ( ( A X. C ) |` { j } ) = ( ( A i^i { j } ) X. ( C i^i _V ) )
18 simpr 
 |-  ( ( ph /\ j e. A ) -> j e. A )
19 18 snssd 
 |-  ( ( ph /\ j e. A ) -> { j } C_ A )
20 sseqin2 
 |-  ( { j } C_ A <-> ( A i^i { j } ) = { j } )
21 19 20 sylib 
 |-  ( ( ph /\ j e. A ) -> ( A i^i { j } ) = { j } )
22 inv1 
 |-  ( C i^i _V ) = C
23 22 a1i 
 |-  ( ( ph /\ j e. A ) -> ( C i^i _V ) = C )
24 21 23 xpeq12d 
 |-  ( ( ph /\ j e. A ) -> ( ( A i^i { j } ) X. ( C i^i _V ) ) = ( { j } X. C ) )
25 17 24 syl5eq 
 |-  ( ( ph /\ j e. A ) -> ( ( A X. C ) |` { j } ) = ( { j } X. C ) )
26 25 rneqd 
 |-  ( ( ph /\ j e. A ) -> ran ( ( A X. C ) |` { j } ) = ran ( { j } X. C ) )
27 vex 
 |-  j e. _V
28 27 snnz 
 |-  { j } =/= (/)
29 rnxp 
 |-  ( { j } =/= (/) -> ran ( { j } X. C ) = C )
30 28 29 ax-mp 
 |-  ran ( { j } X. C ) = C
31 26 30 eqtrdi 
 |-  ( ( ph /\ j e. A ) -> ran ( ( A X. C ) |` { j } ) = C )
32 14 31 syl5eq 
 |-  ( ( ph /\ j e. A ) -> ( ( A X. C ) " { j } ) = C )
33 32 mpteq1d 
 |-  ( ( ph /\ j e. A ) -> ( k e. ( ( A X. C ) " { j } ) |-> ( j F k ) ) = ( k e. C |-> ( j F k ) ) )
34 33 oveq2d 
 |-  ( ( ph /\ j e. A ) -> ( G gsum ( k e. ( ( A X. C ) " { j } ) |-> ( j F k ) ) ) = ( G gsum ( k e. C |-> ( j F k ) ) ) )
35 34 mpteq2dva 
 |-  ( ph -> ( j e. A |-> ( G gsum ( k e. ( ( A X. C ) " { j } ) |-> ( j F k ) ) ) ) = ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) )
36 35 oveq2d 
 |-  ( ph -> ( G gsum ( j e. A |-> ( G gsum ( k e. ( ( A X. C ) " { j } ) |-> ( j F k ) ) ) ) ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) )
37 13 36 eqtrd 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( j e. A |-> ( G gsum ( k e. C |-> ( j F k ) ) ) ) ) )