# Metamath Proof Explorer

## Theorem gsummpt2co

Description: Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Hypotheses gsummpt2co.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
gsummpt2co.z
gsummpt2co.w ${⊢}{\phi }\to {W}\in \mathrm{CMnd}$
gsummpt2co.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsummpt2co.e ${⊢}{\phi }\to {E}\in {V}$
gsummpt2co.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {B}$
gsummpt2co.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {D}\in {E}$
gsummpt2co.3 ${⊢}{F}=\left({x}\in {A}⟼{D}\right)$
Assertion gsummpt2co ${⊢}{\phi }\to \underset{{x}\in {A}}{{\sum }_{{W}}}{C}=\underset{{y}\in {E}}{{\sum }_{{W}}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]}{{\sum }_{{W}}},{C}\right)$

### Proof

Step Hyp Ref Expression
1 gsummpt2co.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 gsummpt2co.z
3 gsummpt2co.w ${⊢}{\phi }\to {W}\in \mathrm{CMnd}$
4 gsummpt2co.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 gsummpt2co.e ${⊢}{\phi }\to {E}\in {V}$
6 gsummpt2co.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {B}$
7 gsummpt2co.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {D}\in {E}$
8 gsummpt2co.3 ${⊢}{F}=\left({x}\in {A}⟼{D}\right)$
9 nfcsb1v
10 csbeq1a
11 ssidd ${⊢}{\phi }\to {B}\subseteq {B}$
12 elcnv ${⊢}{p}\in {{F}}^{-1}↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{z},{x}⟩\wedge {x}{F}{z}\right)$
13 vex ${⊢}{z}\in \mathrm{V}$
14 vex ${⊢}{x}\in \mathrm{V}$
15 13 14 op2ndd ${⊢}{p}=⟨{z},{x}⟩\to {2}^{nd}\left({p}\right)={x}$
16 15 adantr ${⊢}\left({p}=⟨{z},{x}⟩\wedge {x}{F}{z}\right)\to {2}^{nd}\left({p}\right)={x}$
17 8 dmmptss ${⊢}\mathrm{dom}{F}\subseteq {A}$
18 14 13 breldm ${⊢}{x}{F}{z}\to {x}\in \mathrm{dom}{F}$
19 17 18 sseldi ${⊢}{x}{F}{z}\to {x}\in {A}$
20 19 adantl ${⊢}\left({p}=⟨{z},{x}⟩\wedge {x}{F}{z}\right)\to {x}\in {A}$
21 16 20 eqeltrd ${⊢}\left({p}=⟨{z},{x}⟩\wedge {x}{F}{z}\right)\to {2}^{nd}\left({p}\right)\in {A}$
22 21 exlimivv ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{z},{x}⟩\wedge {x}{F}{z}\right)\to {2}^{nd}\left({p}\right)\in {A}$
23 12 22 sylbi ${⊢}{p}\in {{F}}^{-1}\to {2}^{nd}\left({p}\right)\in {A}$
24 23 adantl ${⊢}\left({\phi }\wedge {p}\in {{F}}^{-1}\right)\to {2}^{nd}\left({p}\right)\in {A}$
25 8 funmpt2 ${⊢}\mathrm{Fun}{F}$
26 funcnvcnv ${⊢}\mathrm{Fun}{F}\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
27 25 26 ax-mp ${⊢}\mathrm{Fun}{{{F}}^{-1}}^{-1}$
28 27 a1i ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \mathrm{Fun}{{{F}}^{-1}}^{-1}$
29 dfdm4 ${⊢}\mathrm{dom}{F}=\mathrm{ran}{{F}}^{-1}$
30 8 dmeqi ${⊢}\mathrm{dom}{F}=\mathrm{dom}\left({x}\in {A}⟼{D}\right)$
31 7 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{D}\in {E}$
32 dmmptg ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{D}\in {E}\to \mathrm{dom}\left({x}\in {A}⟼{D}\right)={A}$
33 31 32 syl ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{D}\right)={A}$
34 30 33 syl5eq ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
35 29 34 syl5eqr ${⊢}{\phi }\to \mathrm{ran}{{F}}^{-1}={A}$
36 35 eleq2d ${⊢}{\phi }\to \left({x}\in \mathrm{ran}{{F}}^{-1}↔{x}\in {A}\right)$
37 36 biimpar ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {x}\in \mathrm{ran}{{F}}^{-1}$
38 relcnv ${⊢}\mathrm{Rel}{{F}}^{-1}$
39 fcnvgreu ${⊢}\left(\left(\mathrm{Rel}{{F}}^{-1}\wedge \mathrm{Fun}{{{F}}^{-1}}^{-1}\right)\wedge {x}\in \mathrm{ran}{{F}}^{-1}\right)\to \exists !{p}\in {{F}}^{-1}\phantom{\rule{.4em}{0ex}}{x}={2}^{nd}\left({p}\right)$
40 38 39 mpanl1 ${⊢}\left(\mathrm{Fun}{{{F}}^{-1}}^{-1}\wedge {x}\in \mathrm{ran}{{F}}^{-1}\right)\to \exists !{p}\in {{F}}^{-1}\phantom{\rule{.4em}{0ex}}{x}={2}^{nd}\left({p}\right)$
41 28 37 40 syl2anc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists !{p}\in {{F}}^{-1}\phantom{\rule{.4em}{0ex}}{x}={2}^{nd}\left({p}\right)$
42 9 1 2 10 3 4 11 6 24 41 gsummptf1o
43 8 rnmptss ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{D}\in {E}\to \mathrm{ran}{F}\subseteq {E}$
44 31 43 syl ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq {E}$
45 dfcnv2 ${⊢}\mathrm{ran}{F}\subseteq {E}\to {{F}}^{-1}=\bigcup _{{z}\in {E}}\left(\left\{{z}\right\}×{{F}}^{-1}\left[\left\{{z}\right\}\right]\right)$
46 44 45 syl ${⊢}{\phi }\to {{F}}^{-1}=\bigcup _{{z}\in {E}}\left(\left\{{z}\right\}×{{F}}^{-1}\left[\left\{{z}\right\}\right]\right)$
47 46 mpteq1d
48 nfcv
49 csbeq1
50 15 49 syl
51 csbid
52 50 51 syl6eq
53 48 9 52 mpomptxf
54 47 53 syl6eq
55 54 oveq2d
56 mptfi ${⊢}{A}\in \mathrm{Fin}\to \left({x}\in {A}⟼{D}\right)\in \mathrm{Fin}$
57 8 56 eqeltrid ${⊢}{A}\in \mathrm{Fin}\to {F}\in \mathrm{Fin}$
58 cnvfi ${⊢}{F}\in \mathrm{Fin}\to {{F}}^{-1}\in \mathrm{Fin}$
59 4 57 58 3syl ${⊢}{\phi }\to {{F}}^{-1}\in \mathrm{Fin}$
60 imaexg ${⊢}{{F}}^{-1}\in \mathrm{Fin}\to {{F}}^{-1}\left[\left\{{z}\right\}\right]\in \mathrm{V}$
61 59 60 syl ${⊢}{\phi }\to {{F}}^{-1}\left[\left\{{z}\right\}\right]\in \mathrm{V}$
62 61 adantr ${⊢}\left({\phi }\wedge {z}\in {E}\right)\to {{F}}^{-1}\left[\left\{{z}\right\}\right]\in \mathrm{V}$
63 simpll ${⊢}\left(\left({\phi }\wedge {z}\in {E}\right)\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\to {\phi }$
64 imassrn ${⊢}{{F}}^{-1}\left[\left\{{z}\right\}\right]\subseteq \mathrm{ran}{{F}}^{-1}$
65 64 29 sseqtrri ${⊢}{{F}}^{-1}\left[\left\{{z}\right\}\right]\subseteq \mathrm{dom}{F}$
66 65 17 sstri ${⊢}{{F}}^{-1}\left[\left\{{z}\right\}\right]\subseteq {A}$
67 13 14 elimasn ${⊢}{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]↔⟨{z},{x}⟩\in {{F}}^{-1}$
68 67 biimpi ${⊢}{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\to ⟨{z},{x}⟩\in {{F}}^{-1}$
69 68 adantl ${⊢}\left(\left({\phi }\wedge {z}\in {E}\right)\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\to ⟨{z},{x}⟩\in {{F}}^{-1}$
70 69 67 sylibr ${⊢}\left(\left({\phi }\wedge {z}\in {E}\right)\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\to {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]$
71 66 70 sseldi ${⊢}\left(\left({\phi }\wedge {z}\in {E}\right)\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\to {x}\in {A}$
72 63 71 6 syl2anc ${⊢}\left(\left({\phi }\wedge {z}\in {E}\right)\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\to {C}\in {B}$
73 72 anasss ${⊢}\left({\phi }\wedge \left({z}\in {E}\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\right)\to {C}\in {B}$
74 df-br ${⊢}{z}{{F}}^{-1}{x}↔⟨{z},{x}⟩\in {{F}}^{-1}$
75 69 74 sylibr ${⊢}\left(\left({\phi }\wedge {z}\in {E}\right)\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\to {z}{{F}}^{-1}{x}$
76 75 anasss ${⊢}\left({\phi }\wedge \left({z}\in {E}\wedge {x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]\right)\right)\to {z}{{F}}^{-1}{x}$
77 76 pm2.24d
78 77 imp
79 78 anasss
80 1 2 3 5 62 73 59 79 gsum2d2 ${⊢}{\phi }\to {\sum }_{{W}}\left({z}\in {E},{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]⟼{C}\right)=\underset{{z}\in {E}}{{\sum }_{{W}}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]}{{\sum }_{{W}}},{C}\right)$
81 42 55 80 3eqtrd ${⊢}{\phi }\to \underset{{x}\in {A}}{{\sum }_{{W}}}{C}=\underset{{z}\in {E}}{{\sum }_{{W}}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]}{{\sum }_{{W}}},{C}\right)$
82 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]}{{\sum }_{{W}}},{C}\right)$
83 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]}{{\sum }_{{W}}},{C}\right)$
84 sneq ${⊢}{y}={z}\to \left\{{y}\right\}=\left\{{z}\right\}$
85 84 imaeq2d ${⊢}{y}={z}\to {{F}}^{-1}\left[\left\{{y}\right\}\right]={{F}}^{-1}\left[\left\{{z}\right\}\right]$
86 85 mpteq1d ${⊢}{y}={z}\to \left({x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]⟼{C}\right)=\left({x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]⟼{C}\right)$
87 86 oveq2d ${⊢}{y}={z}\to \underset{{x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]}{{\sum }_{{W}}}{C}=\underset{{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]}{{\sum }_{{W}}}{C}$
88 82 83 87 cbvmpt ${⊢}\left({y}\in {E}⟼\underset{{x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]}{{\sum }_{{W}}}{C}\right)=\left({z}\in {E}⟼\underset{{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]}{{\sum }_{{W}}}{C}\right)$
89 88 oveq2i ${⊢}\underset{{y}\in {E}}{{\sum }_{{W}}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]}{{\sum }_{{W}}},{C}\right)=\underset{{z}\in {E}}{{\sum }_{{W}}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{z}\right\}\right]}{{\sum }_{{W}}},{C}\right)$
90 81 89 syl6eqr ${⊢}{\phi }\to \underset{{x}\in {A}}{{\sum }_{{W}}}{C}=\underset{{y}\in {E}}{{\sum }_{{W}}}\left(\underset{{x}\in {{F}}^{-1}\left[\left\{{y}\right\}\right]}{{\sum }_{{W}}},{C}\right)$