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 ˙ = 0 G
gsumxp.g φ G CMnd
gsumxp.a φ A V
gsumxp.r φ C W
gsumxp.f φ F : A × C B
gsumxp.w φ finSupp 0 ˙ F
Assertion gsumxp φ G F = G j A G k C j F k

Proof

Step Hyp Ref Expression
1 gsumxp.b B = Base G
2 gsumxp.z 0 ˙ = 0 G
3 gsumxp.g φ G CMnd
4 gsumxp.a φ A V
5 gsumxp.r φ C W
6 gsumxp.f φ F : A × C B
7 gsumxp.w φ finSupp 0 ˙ F
8 4 5 xpexd φ A × C V
9 relxp Rel A × C
10 9 a1i φ Rel A × C
11 dmxpss dom A × C A
12 11 a1i φ dom A × C A
13 1 2 3 8 10 4 12 6 7 gsum2d φ G F = G j A G k A × C j j F k
14 df-ima A × C j = ran A × C j
15 df-res A × C j = A × C j × V
16 inxp A × C j × V = A j × C V
17 15 16 eqtri A × C j = A j × C V
18 simpr φ j A j A
19 18 snssd φ j A j A
20 sseqin2 j A A j = j
21 19 20 sylib φ j A A j = j
22 inv1 C V = C
23 22 a1i φ j A C V = C
24 21 23 xpeq12d φ j A A j × C V = j × C
25 17 24 syl5eq φ j A A × C j = j × C
26 25 rneqd φ j A ran A × C j = ran j × C
27 vex j V
28 27 snnz j
29 rnxp j ran j × C = C
30 28 29 ax-mp ran j × C = C
31 26 30 syl6eq φ j A ran A × C j = C
32 14 31 syl5eq φ j A A × C j = C
33 32 mpteq1d φ j A k A × C j j F k = k C j F k
34 33 oveq2d φ j A G k A × C j j F k = G k C j F k
35 34 mpteq2dva φ j A G k A × C j j F k = j A G k C j F k
36 35 oveq2d φ G j A G k A × C j j F k = G j A G k C j F k
37 13 36 eqtrd φ G F = G j A G k C j F k