# Metamath Proof Explorer

## Theorem psrass1lem

Description: A group sum commutation used by psrass1 . (Contributed by Mario Carneiro, 5-Jan-2015)

Ref Expression
Hypotheses psrbag.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
psrbagconf1o.1 ${⊢}{S}=\left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}$
gsumbagdiag.i ${⊢}{\phi }\to {I}\in {V}$
gsumbagdiag.f ${⊢}{\phi }\to {F}\in {D}$
gsumbagdiag.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsumbagdiag.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsumbagdiag.x ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {X}\in {B}$
psrass1lem.y ${⊢}{k}={n}{-}_{f}{j}\to {X}={Y}$
Assertion psrass1lem ${⊢}{\phi }\to \underset{{n}\in {S}}{{\sum }_{{G}}}\left(\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}},{Y}\right)=\underset{{j}\in {S}}{{\sum }_{{G}}}\left(\underset{{k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}}{{\sum }_{{G}}},{X}\right)$

### Proof

Step Hyp Ref Expression
1 psrbag.d ${⊢}{D}=\left\{{f}\in \left({{ℕ}_{0}}^{{I}}\right)|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
2 psrbagconf1o.1 ${⊢}{S}=\left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}$
3 gsumbagdiag.i ${⊢}{\phi }\to {I}\in {V}$
4 gsumbagdiag.f ${⊢}{\phi }\to {F}\in {D}$
5 gsumbagdiag.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
6 gsumbagdiag.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
7 gsumbagdiag.x ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {X}\in {B}$
8 psrass1lem.y ${⊢}{k}={n}{-}_{f}{j}\to {X}={Y}$
9 1 2 3 4 gsumbagdiaglem ${⊢}\left({\phi }\wedge \left({m}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\right)\right)\to \left({j}\in {S}\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)$
10 7 anassrs ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {X}\in {B}$
11 10 fmpttd ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶{B}$
12 3 adantr ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {I}\in {V}$
13 2 ssrab3 ${⊢}{S}\subseteq {D}$
14 4 adantr ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {F}\in {D}$
15 simpr ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {j}\in {S}$
16 1 2 psrbagconcl ${⊢}\left({I}\in {V}\wedge {F}\in {D}\wedge {j}\in {S}\right)\to {F}{-}_{f}{j}\in {S}$
17 12 14 15 16 syl3anc ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {F}{-}_{f}{j}\in {S}$
18 13 17 sseldi ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {F}{-}_{f}{j}\in {D}$
19 eqid ${⊢}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}=\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
20 1 19 psrbagconf1o ${⊢}\left({I}\in {V}\wedge {F}{-}_{f}{j}\in {D}\right)\to \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\underset{1-1 onto}{⟶}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
21 12 18 20 syl2anc ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\underset{1-1 onto}{⟶}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
22 f1of ${⊢}\left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\underset{1-1 onto}{⟶}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\to \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
23 21 22 syl ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
24 fco ${⊢}\left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶{B}\wedge \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\circ \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right)\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶{B}$
25 11 23 24 syl2anc ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\circ \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right)\right):\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟶{B}$
26 12 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {I}\in {V}$
27 14 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {F}\in {D}$
28 1 psrbagf ${⊢}\left({I}\in {V}\wedge {F}\in {D}\right)\to {F}:{I}⟶{ℕ}_{0}$
29 26 27 28 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {F}:{I}⟶{ℕ}_{0}$
30 29 ffvelrnda ${⊢}\left(\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge {z}\in {I}\right)\to {F}\left({z}\right)\in {ℕ}_{0}$
31 15 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {j}\in {S}$
32 13 31 sseldi ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {j}\in {D}$
33 1 psrbagf ${⊢}\left({I}\in {V}\wedge {j}\in {D}\right)\to {j}:{I}⟶{ℕ}_{0}$
34 26 32 33 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {j}:{I}⟶{ℕ}_{0}$
35 34 ffvelrnda ${⊢}\left(\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge {z}\in {I}\right)\to {j}\left({z}\right)\in {ℕ}_{0}$
36 ssrab2 ${⊢}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\subseteq {D}$
37 simpr ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
38 36 37 sseldi ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {m}\in {D}$
39 1 psrbagf ${⊢}\left({I}\in {V}\wedge {m}\in {D}\right)\to {m}:{I}⟶{ℕ}_{0}$
40 26 38 39 syl2anc ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {m}:{I}⟶{ℕ}_{0}$
41 40 ffvelrnda ${⊢}\left(\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge {z}\in {I}\right)\to {m}\left({z}\right)\in {ℕ}_{0}$
42 nn0cn ${⊢}{F}\left({z}\right)\in {ℕ}_{0}\to {F}\left({z}\right)\in ℂ$
43 nn0cn ${⊢}{j}\left({z}\right)\in {ℕ}_{0}\to {j}\left({z}\right)\in ℂ$
44 nn0cn ${⊢}{m}\left({z}\right)\in {ℕ}_{0}\to {m}\left({z}\right)\in ℂ$
45 sub32 ${⊢}\left({F}\left({z}\right)\in ℂ\wedge {j}\left({z}\right)\in ℂ\wedge {m}\left({z}\right)\in ℂ\right)\to {F}\left({z}\right)-{j}\left({z}\right)-{m}\left({z}\right)={F}\left({z}\right)-{m}\left({z}\right)-{j}\left({z}\right)$
46 42 43 44 45 syl3an ${⊢}\left({F}\left({z}\right)\in {ℕ}_{0}\wedge {j}\left({z}\right)\in {ℕ}_{0}\wedge {m}\left({z}\right)\in {ℕ}_{0}\right)\to {F}\left({z}\right)-{j}\left({z}\right)-{m}\left({z}\right)={F}\left({z}\right)-{m}\left({z}\right)-{j}\left({z}\right)$
47 30 35 41 46 syl3anc ${⊢}\left(\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge {z}\in {I}\right)\to {F}\left({z}\right)-{j}\left({z}\right)-{m}\left({z}\right)={F}\left({z}\right)-{m}\left({z}\right)-{j}\left({z}\right)$
48 47 mpteq2dva ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({z}\in {I}⟼{F}\left({z}\right)-{j}\left({z}\right)-{m}\left({z}\right)\right)=\left({z}\in {I}⟼{F}\left({z}\right)-{m}\left({z}\right)-{j}\left({z}\right)\right)$
49 ovexd ${⊢}\left(\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge {z}\in {I}\right)\to {F}\left({z}\right)-{j}\left({z}\right)\in \mathrm{V}$
50 29 feqmptd ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {F}=\left({z}\in {I}⟼{F}\left({z}\right)\right)$
51 34 feqmptd ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {j}=\left({z}\in {I}⟼{j}\left({z}\right)\right)$
52 26 30 35 50 51 offval2 ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {F}{-}_{f}{j}=\left({z}\in {I}⟼{F}\left({z}\right)-{j}\left({z}\right)\right)$
53 40 feqmptd ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {m}=\left({z}\in {I}⟼{m}\left({z}\right)\right)$
54 26 49 41 52 53 offval2 ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({F}{-}_{f}{j}\right){-}_{f}{m}=\left({z}\in {I}⟼{F}\left({z}\right)-{j}\left({z}\right)-{m}\left({z}\right)\right)$
55 ovexd ${⊢}\left(\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\wedge {z}\in {I}\right)\to {F}\left({z}\right)-{m}\left({z}\right)\in \mathrm{V}$
56 26 30 41 50 53 offval2 ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {F}{-}_{f}{m}=\left({z}\in {I}⟼{F}\left({z}\right)-{m}\left({z}\right)\right)$
57 26 55 35 56 51 offval2 ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({F}{-}_{f}{m}\right){-}_{f}{j}=\left({z}\in {I}⟼{F}\left({z}\right)-{m}\left({z}\right)-{j}\left({z}\right)\right)$
58 48 54 57 3eqtr4d ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({F}{-}_{f}{j}\right){-}_{f}{m}=\left({F}{-}_{f}{m}\right){-}_{f}{j}$
59 18 adantr ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to {F}{-}_{f}{j}\in {D}$
60 1 19 psrbagconcl ${⊢}\left({I}\in {V}\wedge {F}{-}_{f}{j}\in {D}\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({F}{-}_{f}{j}\right){-}_{f}{m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
61 26 59 37 60 syl3anc ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({F}{-}_{f}{j}\right){-}_{f}{m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
62 58 61 eqeltrrd ${⊢}\left(\left({\phi }\wedge {j}\in {S}\right)\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\to \left({F}{-}_{f}{m}\right){-}_{f}{j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
63 58 mpteq2dva ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right)=\left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{m}\right){-}_{f}{j}\right)$
64 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{X}$
65 nfcsb1v
66 csbeq1a
67 64 65 66 cbvmpt
68 67 a1i
69 csbeq1
70 62 63 68 69 fmptco
71 70 feq1d
72 25 71 mpbid
73 72 fvmptelrn
74 73 anasss
75 9 74 syldan
76 1 2 3 4 5 6 75 gsumbagdiag
77 eqid ${⊢}{0}_{{G}}={0}_{{G}}$
78 1 psrbaglefi ${⊢}\left({I}\in {V}\wedge {F}\in {D}\right)\to \left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}\in \mathrm{Fin}$
79 3 4 78 syl2anc ${⊢}{\phi }\to \left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}\in \mathrm{Fin}$
80 2 79 eqeltrid ${⊢}{\phi }\to {S}\in \mathrm{Fin}$
81 3 adantr ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {I}\in {V}$
82 4 adantr ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {F}\in {D}$
83 simpr ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {m}\in {S}$
84 1 2 psrbagconcl ${⊢}\left({I}\in {V}\wedge {F}\in {D}\wedge {m}\in {S}\right)\to {F}{-}_{f}{m}\in {S}$
85 81 82 83 84 syl3anc ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {F}{-}_{f}{m}\in {S}$
86 13 85 sseldi ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {F}{-}_{f}{m}\in {D}$
87 1 psrbaglefi ${⊢}\left({I}\in {V}\wedge {F}{-}_{f}{m}\in {D}\right)\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\in \mathrm{Fin}$
88 81 86 87 syl2anc ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\in \mathrm{Fin}$
89 xpfi ${⊢}\left({S}\in \mathrm{Fin}\wedge {S}\in \mathrm{Fin}\right)\to {S}×{S}\in \mathrm{Fin}$
90 80 80 89 syl2anc ${⊢}{\phi }\to {S}×{S}\in \mathrm{Fin}$
91 simprl ${⊢}\left({\phi }\wedge \left({m}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\right)\right)\to {m}\in {S}$
92 9 simpld ${⊢}\left({\phi }\wedge \left({m}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\right)\right)\to {j}\in {S}$
93 brxp ${⊢}{m}\left({S}×{S}\right){j}↔\left({m}\in {S}\wedge {j}\in {S}\right)$
94 91 92 93 sylanbrc ${⊢}\left({\phi }\wedge \left({m}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\right)\right)\to {m}\left({S}×{S}\right){j}$
95 94 pm2.24d
96 95 impr
97 5 77 6 80 88 75 90 96 gsum2d2
98 1 psrbaglefi ${⊢}\left({I}\in {V}\wedge {F}{-}_{f}{j}\in {D}\right)\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{Fin}$
99 12 18 98 syl2anc ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{Fin}$
100 simprl ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {j}\in {S}$
101 1 2 3 4 gsumbagdiaglem ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to \left({m}\in {S}\wedge {j}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\right)$
102 101 simpld ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {m}\in {S}$
103 brxp ${⊢}{j}\left({S}×{S}\right){m}↔\left({j}\in {S}\wedge {m}\in {S}\right)$
104 100 102 103 sylanbrc ${⊢}\left({\phi }\wedge \left({j}\in {S}\wedge {m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {j}\left({S}×{S}\right){m}$
105 104 pm2.24d
106 105 impr
107 5 77 6 80 99 74 90 106 gsum2d2
108 76 97 107 3eqtr3d
109 6 adantr ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {G}\in \mathrm{CMnd}$
110 75 anassrs
111 110 fmpttd
112 ovex ${⊢}{{ℕ}_{0}}^{{I}}\in \mathrm{V}$
113 1 112 rabex2 ${⊢}{D}\in \mathrm{V}$
114 113 a1i ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {D}\in \mathrm{V}$
115 rabexg ${⊢}{D}\in \mathrm{V}\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}\in \mathrm{V}$
116 mptexg
117 114 115 116 3syl
118 funmpt
119 118 a1i
120 fvexd ${⊢}\left({\phi }\wedge {m}\in {S}\right)\to {0}_{{G}}\in \mathrm{V}$
121 suppssdm
122 eqid
123 122 dmmptss
124 121 123 sstri
125 124 a1i
126 suppssfifsupp
127 117 119 120 88 125 126 syl32anc
128 5 77 109 88 111 127 gsumcl
129 128 fmpttd
130 1 2 psrbagconf1o ${⊢}\left({I}\in {V}\wedge {F}\in {D}\right)\to \left({m}\in {S}⟼{F}{-}_{f}{m}\right):{S}\underset{1-1 onto}{⟶}{S}$
131 3 4 130 syl2anc ${⊢}{\phi }\to \left({m}\in {S}⟼{F}{-}_{f}{m}\right):{S}\underset{1-1 onto}{⟶}{S}$
132 f1ocnv ${⊢}\left({m}\in {S}⟼{F}{-}_{f}{m}\right):{S}\underset{1-1 onto}{⟶}{S}\to {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}:{S}\underset{1-1 onto}{⟶}{S}$
133 f1of ${⊢}{\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}:{S}\underset{1-1 onto}{⟶}{S}\to {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}:{S}⟶{S}$
134 131 132 133 3syl ${⊢}{\phi }\to {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}:{S}⟶{S}$
135 fco
136 129 134 135 syl2anc
137 coass ${⊢}\left(\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({m}\in {S}⟼{F}{-}_{f}{m}\right)\right)\circ {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left(\left({m}\in {S}⟼{F}{-}_{f}{m}\right)\circ {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}\right)$
138 f1ococnv2 ${⊢}\left({m}\in {S}⟼{F}{-}_{f}{m}\right):{S}\underset{1-1 onto}{⟶}{S}\to \left({m}\in {S}⟼{F}{-}_{f}{m}\right)\circ {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}={\mathrm{I}↾}_{{S}}$
139 131 138 syl ${⊢}{\phi }\to \left({m}\in {S}⟼{F}{-}_{f}{m}\right)\circ {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}={\mathrm{I}↾}_{{S}}$
140 139 coeq2d ${⊢}{\phi }\to \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left(\left({m}\in {S}⟼{F}{-}_{f}{m}\right)\circ {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}\right)=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({\mathrm{I}↾}_{{S}}\right)$
141 137 140 syl5eq ${⊢}{\phi }\to \left(\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({m}\in {S}⟼{F}{-}_{f}{m}\right)\right)\circ {\left({m}\in {S}⟼{F}{-}_{f}{m}\right)}^{-1}=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({\mathrm{I}↾}_{{S}}\right)$
142 eqidd ${⊢}{\phi }\to \left({m}\in {S}⟼{F}{-}_{f}{m}\right)=\left({m}\in {S}⟼{F}{-}_{f}{m}\right)$
143 eqidd ${⊢}{\phi }\to \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
144 breq2 ${⊢}{n}={F}{-}_{f}{m}\to \left({x}{\le }_{f}{n}↔{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right)$
145 144 rabbidv ${⊢}{n}={F}{-}_{f}{m}\to \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}=\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{m}\right)\right\}$
146 ovex ${⊢}{n}{-}_{f}{j}\in \mathrm{V}$
147 146 8 csbie
148 oveq1 ${⊢}{n}={F}{-}_{f}{m}\to {n}{-}_{f}{j}=\left({F}{-}_{f}{m}\right){-}_{f}{j}$
149 148 csbeq1d
150 147 149 syl5eqr
151 145 150 mpteq12dv
152 151 oveq2d
153 85 142 143 152 fmptco
154 153 coeq1d
155 coires1 ${⊢}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({\mathrm{I}↾}_{{S}}\right)={\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)↾}_{{S}}$
156 ssid ${⊢}{S}\subseteq {S}$
157 resmpt ${⊢}{S}\subseteq {S}\to {\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)↾}_{{S}}=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
158 156 157 ax-mp ${⊢}{\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)↾}_{{S}}=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
159 155 158 eqtri ${⊢}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({\mathrm{I}↾}_{{S}}\right)=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
160 159 a1i ${⊢}{\phi }\to \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({\mathrm{I}↾}_{{S}}\right)=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
161 141 154 160 3eqtr3d
162 161 feq1d
163 136 162 mpbid ${⊢}{\phi }\to \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right):{S}⟶{B}$
164 rabexg ${⊢}{D}\in \mathrm{V}\to \left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}\in \mathrm{V}$
165 113 164 mp1i ${⊢}{\phi }\to \left\{{y}\in {D}|{y}{\le }_{f}{F}\right\}\in \mathrm{V}$
166 2 165 eqeltrid ${⊢}{\phi }\to {S}\in \mathrm{V}$
167 166 mptexd ${⊢}{\phi }\to \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\in \mathrm{V}$
168 funmpt ${⊢}\mathrm{Fun}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
169 168 a1i ${⊢}{\phi }\to \mathrm{Fun}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
170 fvexd ${⊢}{\phi }\to {0}_{{G}}\in \mathrm{V}$
171 suppssdm ${⊢}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\mathrm{supp}{0}_{{G}}\subseteq \mathrm{dom}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
172 eqid ${⊢}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)=\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)$
173 172 dmmptss ${⊢}\mathrm{dom}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\subseteq {S}$
174 171 173 sstri ${⊢}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\mathrm{supp}{0}_{{G}}\subseteq {S}$
175 174 a1i ${⊢}{\phi }\to \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\mathrm{supp}{0}_{{G}}\subseteq {S}$
176 suppssfifsupp ${⊢}\left(\left(\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\in \mathrm{V}\wedge \mathrm{Fun}\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\wedge {0}_{{G}}\in \mathrm{V}\right)\wedge \left({S}\in \mathrm{Fin}\wedge \left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\mathrm{supp}{0}_{{G}}\subseteq {S}\right)\right)\to {finSupp}_{{0}_{{G}}}\left(\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\right)$
177 167 169 170 80 175 176 syl32anc ${⊢}{\phi }\to {finSupp}_{{0}_{{G}}}\left(\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\right)$
178 5 77 6 80 163 177 131 gsumf1o ${⊢}{\phi }\to \underset{{n}\in {S}}{{\sum }_{{G}}}\left(\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}},{Y}\right)={\sum }_{{G}}\left(\left({n}\in {S}⟼\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}}{Y}\right)\circ \left({m}\in {S}⟼{F}{-}_{f}{m}\right)\right)$
179 153 oveq2d
180 178 179 eqtrd
181 6 adantr ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {G}\in \mathrm{CMnd}$
182 113 a1i ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {D}\in \mathrm{V}$
183 rabexg ${⊢}{D}\in \mathrm{V}\to \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{V}$
184 mptexg ${⊢}\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{V}\to \left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\in \mathrm{V}$
185 182 183 184 3syl ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\in \mathrm{V}$
186 funmpt ${⊢}\mathrm{Fun}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)$
187 186 a1i ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \mathrm{Fun}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)$
188 fvexd ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {0}_{{G}}\in \mathrm{V}$
189 suppssdm ${⊢}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\mathrm{supp}{0}_{{G}}\subseteq \mathrm{dom}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)$
190 eqid ${⊢}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)=\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)$
191 190 dmmptss ${⊢}\mathrm{dom}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\subseteq \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
192 189 191 sstri ${⊢}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\mathrm{supp}{0}_{{G}}\subseteq \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
193 192 a1i ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\mathrm{supp}{0}_{{G}}\subseteq \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}$
194 suppssfifsupp ${⊢}\left(\left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\in \mathrm{V}\wedge \mathrm{Fun}\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\wedge {0}_{{G}}\in \mathrm{V}\right)\wedge \left(\left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\in \mathrm{Fin}\wedge \left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\mathrm{supp}{0}_{{G}}\subseteq \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}\right)\right)\to {finSupp}_{{0}_{{G}}}\left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\right)$
195 185 187 188 99 193 194 syl32anc ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to {finSupp}_{{0}_{{G}}}\left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\right)$
196 5 77 181 99 11 195 21 gsumf1o ${⊢}\left({\phi }\wedge {j}\in {S}\right)\to \underset{{k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}}{{\sum }_{{G}}}{X}={\sum }_{{G}}\left(\left({k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼{X}\right)\circ \left({m}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}⟼\left({F}{-}_{f}{j}\right){-}_{f}{m}\right)\right)$
197 70 oveq2d
198 196 197 eqtrd
199 198 mpteq2dva
200 199 oveq2d
201 108 180 200 3eqtr4d ${⊢}{\phi }\to \underset{{n}\in {S}}{{\sum }_{{G}}}\left(\underset{{j}\in \left\{{x}\in {D}|{x}{\le }_{f}{n}\right\}}{{\sum }_{{G}}},{Y}\right)=\underset{{j}\in {S}}{{\sum }_{{G}}}\left(\underset{{k}\in \left\{{x}\in {D}|{x}{\le }_{f}\left({F}{-}_{f}{j}\right)\right\}}{{\sum }_{{G}}},{X}\right)$