# 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}={\mathrm{Base}}_{{G}}$
gsumxp.z
gsumxp.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsumxp.a ${⊢}{\phi }\to {A}\in {V}$
gsumxp.r ${⊢}{\phi }\to {C}\in {W}$
gsumxp.f ${⊢}{\phi }\to {F}:{A}×{C}⟶{B}$
gsumxp.w
Assertion gsumxp ${⊢}{\phi }\to {\sum }_{{G}}{F}=\underset{{j}\in {A}}{{\sum }_{{G}}}\left(\underset{{k}\in {C}}{{\sum }_{{G}}},\left({j}{F}{k}\right)\right)$

### Proof

Step Hyp Ref Expression
1 gsumxp.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 gsumxp.z
3 gsumxp.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
4 gsumxp.a ${⊢}{\phi }\to {A}\in {V}$
5 gsumxp.r ${⊢}{\phi }\to {C}\in {W}$
6 gsumxp.f ${⊢}{\phi }\to {F}:{A}×{C}⟶{B}$
7 gsumxp.w
8 4 5 xpexd ${⊢}{\phi }\to {A}×{C}\in \mathrm{V}$
9 relxp ${⊢}\mathrm{Rel}\left({A}×{C}\right)$
10 9 a1i ${⊢}{\phi }\to \mathrm{Rel}\left({A}×{C}\right)$
11 dmxpss ${⊢}\mathrm{dom}\left({A}×{C}\right)\subseteq {A}$
12 11 a1i ${⊢}{\phi }\to \mathrm{dom}\left({A}×{C}\right)\subseteq {A}$
13 1 2 3 8 10 4 12 6 7 gsum2d ${⊢}{\phi }\to {\sum }_{{G}}{F}=\underset{{j}\in {A}}{{\sum }_{{G}}}\left(\underset{{k}\in \left({A}×{C}\right)\left[\left\{{j}\right\}\right]}{{\sum }_{{G}}},\left({j}{F}{k}\right)\right)$
14 df-ima ${⊢}\left({A}×{C}\right)\left[\left\{{j}\right\}\right]=\mathrm{ran}\left({\left({A}×{C}\right)↾}_{\left\{{j}\right\}}\right)$
15 df-res ${⊢}{\left({A}×{C}\right)↾}_{\left\{{j}\right\}}=\left({A}×{C}\right)\cap \left(\left\{{j}\right\}×\mathrm{V}\right)$
16 inxp ${⊢}\left({A}×{C}\right)\cap \left(\left\{{j}\right\}×\mathrm{V}\right)=\left({A}\cap \left\{{j}\right\}\right)×\left({C}\cap \mathrm{V}\right)$
17 15 16 eqtri ${⊢}{\left({A}×{C}\right)↾}_{\left\{{j}\right\}}=\left({A}\cap \left\{{j}\right\}\right)×\left({C}\cap \mathrm{V}\right)$
18 simpr ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {j}\in {A}$
19 18 snssd ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left\{{j}\right\}\subseteq {A}$
20 sseqin2 ${⊢}\left\{{j}\right\}\subseteq {A}↔{A}\cap \left\{{j}\right\}=\left\{{j}\right\}$
21 19 20 sylib ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {A}\cap \left\{{j}\right\}=\left\{{j}\right\}$
22 inv1 ${⊢}{C}\cap \mathrm{V}={C}$
23 22 a1i ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {C}\cap \mathrm{V}={C}$
24 21 23 xpeq12d ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left({A}\cap \left\{{j}\right\}\right)×\left({C}\cap \mathrm{V}\right)=\left\{{j}\right\}×{C}$
25 17 24 syl5eq ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to {\left({A}×{C}\right)↾}_{\left\{{j}\right\}}=\left\{{j}\right\}×{C}$
26 25 rneqd ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \mathrm{ran}\left({\left({A}×{C}\right)↾}_{\left\{{j}\right\}}\right)=\mathrm{ran}\left(\left\{{j}\right\}×{C}\right)$
27 vex ${⊢}{j}\in \mathrm{V}$
28 27 snnz ${⊢}\left\{{j}\right\}\ne \varnothing$
29 rnxp ${⊢}\left\{{j}\right\}\ne \varnothing \to \mathrm{ran}\left(\left\{{j}\right\}×{C}\right)={C}$
30 28 29 ax-mp ${⊢}\mathrm{ran}\left(\left\{{j}\right\}×{C}\right)={C}$
31 26 30 syl6eq ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \mathrm{ran}\left({\left({A}×{C}\right)↾}_{\left\{{j}\right\}}\right)={C}$
32 14 31 syl5eq ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left({A}×{C}\right)\left[\left\{{j}\right\}\right]={C}$
33 32 mpteq1d ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \left({k}\in \left({A}×{C}\right)\left[\left\{{j}\right\}\right]⟼{j}{F}{k}\right)=\left({k}\in {C}⟼{j}{F}{k}\right)$
34 33 oveq2d ${⊢}\left({\phi }\wedge {j}\in {A}\right)\to \underset{{k}\in \left({A}×{C}\right)\left[\left\{{j}\right\}\right]}{{\sum }_{{G}}}\left({j}{F}{k}\right)=\underset{{k}\in {C}}{{\sum }_{{G}}}\left({j}{F}{k}\right)$
35 34 mpteq2dva ${⊢}{\phi }\to \left({j}\in {A}⟼\underset{{k}\in \left({A}×{C}\right)\left[\left\{{j}\right\}\right]}{{\sum }_{{G}}}\left({j}{F}{k}\right)\right)=\left({j}\in {A}⟼\underset{{k}\in {C}}{{\sum }_{{G}}}\left({j}{F}{k}\right)\right)$
36 35 oveq2d ${⊢}{\phi }\to \underset{{j}\in {A}}{{\sum }_{{G}}}\left(\underset{{k}\in \left({A}×{C}\right)\left[\left\{{j}\right\}\right]}{{\sum }_{{G}}},\left({j}{F}{k}\right)\right)=\underset{{j}\in {A}}{{\sum }_{{G}}}\left(\underset{{k}\in {C}}{{\sum }_{{G}}},\left({j}{F}{k}\right)\right)$
37 13 36 eqtrd ${⊢}{\phi }\to {\sum }_{{G}}{F}=\underset{{j}\in {A}}{{\sum }_{{G}}}\left(\underset{{k}\in {C}}{{\sum }_{{G}}},\left({j}{F}{k}\right)\right)$