Metamath Proof Explorer


Theorem xrge0tsmsd

Description: Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015) (Revised by Thierry Arnoux, 30-Jan-2017)

Ref Expression
Hypotheses xrge0tsmsd.g G=𝑠*𝑠0+∞
xrge0tsmsd.a φAV
xrge0tsmsd.f φF:A0+∞
xrge0tsmsd.s φS=suprans𝒫AFinGFs*<
Assertion xrge0tsmsd φGtsumsF=S

Proof

Step Hyp Ref Expression
1 xrge0tsmsd.g G=𝑠*𝑠0+∞
2 xrge0tsmsd.a φAV
3 xrge0tsmsd.f φF:A0+∞
4 xrge0tsmsd.s φS=suprans𝒫AFinGFs*<
5 iccssxr 0+∞*
6 xrsbas *=Base𝑠*
7 1 6 ressbas2 0+∞*0+∞=BaseG
8 5 7 ax-mp 0+∞=BaseG
9 eqid 0G=0G
10 xrge0cmn 𝑠*𝑠0+∞CMnd
11 1 10 eqeltri GCMnd
12 11 a1i φs𝒫AFinGCMnd
13 simpr φs𝒫AFins𝒫AFin
14 elfpw s𝒫AFinsAsFin
15 14 simplbi s𝒫AFinsA
16 fssres F:A0+∞sAFs:s0+∞
17 3 15 16 syl2an φs𝒫AFinFs:s0+∞
18 elinel2 s𝒫AFinsFin
19 18 adantl φs𝒫AFinsFin
20 fvexd φs𝒫AFin0GV
21 17 19 20 fdmfifsupp φs𝒫AFinfinSupp0GFs
22 8 9 12 13 17 21 gsumcl φs𝒫AFinGFs0+∞
23 5 22 sselid φs𝒫AFinGFs*
24 23 fmpttd φs𝒫AFinGFs:𝒫AFin*
25 24 frnd φrans𝒫AFinGFs*
26 supxrcl rans𝒫AFinGFs*suprans𝒫AFinGFs*<*
27 25 26 syl φsuprans𝒫AFinGFs*<*
28 4 27 eqeltrd φS*
29 0ss A
30 0fin Fin
31 elfpw 𝒫AFinAFin
32 29 30 31 mpbir2an 𝒫AFin
33 0cn 0
34 eqid s𝒫AFinGFs=s𝒫AFinGFs
35 reseq2 s=Fs=F
36 res0 F=
37 35 36 eqtrdi s=Fs=
38 37 oveq2d s=GFs=G
39 eqid 𝑠*𝑠*−∞=𝑠*𝑠*−∞
40 39 xrge0subm 0+∞SubMnd𝑠*𝑠*−∞
41 xrex *V
42 difexg *V*−∞V
43 41 42 ax-mp *−∞V
44 simpl x*0xx*
45 ge0nemnf x*0xx−∞
46 44 45 jca x*0xx*x−∞
47 elxrge0 x0+∞x*0x
48 eldifsn x*−∞x*x−∞
49 46 47 48 3imtr4i x0+∞x*−∞
50 49 ssriv 0+∞*−∞
51 ressabs *−∞V0+∞*−∞𝑠*𝑠*−∞𝑠0+∞=𝑠*𝑠0+∞
52 43 50 51 mp2an 𝑠*𝑠*−∞𝑠0+∞=𝑠*𝑠0+∞
53 1 52 eqtr4i G=𝑠*𝑠*−∞𝑠0+∞
54 39 xrs10 0=0𝑠*𝑠*−∞
55 53 54 subm0 0+∞SubMnd𝑠*𝑠*−∞0=0G
56 40 55 ax-mp 0=0G
57 56 gsum0 G=0
58 38 57 eqtrdi s=GFs=0
59 34 58 elrnmpt1s 𝒫AFin00rans𝒫AFinGFs
60 32 33 59 mp2an 0rans𝒫AFinGFs
61 supxrub rans𝒫AFinGFs*0rans𝒫AFinGFs0suprans𝒫AFinGFs*<
62 25 60 61 sylancl φ0suprans𝒫AFinGFs*<
63 62 4 breqtrrd φ0S
64 elxrge0 S0+∞S*0S
65 28 63 64 sylanbrc φS0+∞
66 letop ordTopTop
67 ovex 0+∞V
68 elrest ordTopTop0+∞VuordTop𝑡0+∞vordTopu=v0+∞
69 66 67 68 mp2an uordTop𝑡0+∞vordTopu=v0+∞
70 elinel1 Sv0+∞Sv
71 simplrl φvordTopSvSvordTop
72 reex V
73 elrestr ordTopTopVvordTopvordTop𝑡
74 66 72 73 mp3an12 vordTopvordTop𝑡
75 71 74 syl φvordTopSvSvordTop𝑡
76 eqid ordTop𝑡=ordTop𝑡
77 76 xrtgioo topGenran.=ordTop𝑡
78 75 77 eleqtrrdi φvordTopSvSvtopGenran.
79 simplrr φvordTopSvSSv
80 simpr φvordTopSvSS
81 79 80 elind φvordTopSvSSv
82 tg2 vtopGenran.Svuran.Suuv
83 78 81 82 syl2anc φvordTopSvSuran.Suuv
84 ioof .:*×*𝒫
85 ffn .:*×*𝒫.Fn*×*
86 ovelrn .Fn*×*uran.r*w*u=rw
87 84 85 86 mp2b uran.r*w*u=rw
88 simprrr φvordTopSvSr*w*Srwrwvrwv
89 88 adantr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyrwv
90 inss1 vv
91 89 90 sstrdi φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyrwv
92 11 a1i φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGCMnd
93 simprrl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyy𝒫AFin
94 elinel2 y𝒫AFinyFin
95 93 94 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyyFin
96 simp-4l φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyφ
97 96 3 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyF:A0+∞
98 elfpw y𝒫AFinyAyFin
99 98 simplbi y𝒫AFinyA
100 93 99 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyyA
101 97 100 fssresd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyFy:y0+∞
102 3 ffund φFunF
103 102 ad2antrr φvordTopSvSFunF
104 103 ad2antrr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyFunF
105 c0ex 0V
106 105 a1i φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzy0V
107 104 95 106 resfifsupp φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyfinSupp0Fy
108 8 56 92 95 101 107 gsumcl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFy0+∞
109 5 108 sselid φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFy*
110 simprll φvordTopSvSr*w*Srwrwvr*
111 110 adantr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyr*
112 simprll φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyz𝒫AFin
113 simprrr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyzy
114 113 100 sstrd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyzA
115 97 114 fssresd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyFz:z0+∞
116 ssfi yFinzyzFin
117 95 113 116 syl2anc φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyzFin
118 fvexd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzy0GV
119 115 117 118 fdmfifsupp φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyfinSupp0GFz
120 8 9 92 112 115 119 gsumcl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFz0+∞
121 5 120 sselid φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFz*
122 simprlr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyr<GFz
123 96 2 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyAV
124 1 123 97 93 113 xrge0gsumle φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFzGFy
125 111 121 109 122 124 xrltletrd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyr<GFy
126 96 28 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyS*
127 simprlr φvordTopSvSr*w*Srwrwvw*
128 127 adantr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyw*
129 96 25 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyrans𝒫AFinGFs*
130 ovex GFyV
131 reseq2 s=yFs=Fy
132 131 oveq2d s=yGFs=GFy
133 34 132 elrnmpt1s y𝒫AFinGFyVGFyrans𝒫AFinGFs
134 93 130 133 sylancl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyrans𝒫AFinGFs
135 supxrub rans𝒫AFinGFs*GFyrans𝒫AFinGFsGFysuprans𝒫AFinGFs*<
136 129 134 135 syl2anc φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFysuprans𝒫AFinGFs*<
137 96 4 syl φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyS=suprans𝒫AFinGFs*<
138 136 137 breqtrrd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyS
139 simprrl φvordTopSvSr*w*SrwrwvSrw
140 eliooord Srwr<SS<w
141 139 140 syl φvordTopSvSr*w*Srwrwvr<SS<w
142 141 simprd φvordTopSvSr*w*SrwrwvS<w
143 142 adantr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyS<w
144 109 126 128 138 143 xrlelttrd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFy<w
145 elioo1 r*w*GFyrwGFy*r<GFyGFy<w
146 111 128 145 syl2anc φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyrwGFy*r<GFyGFy<w
147 109 125 144 146 mpbir3and φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyrw
148 91 147 sseldd φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyv
149 148 108 elind φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
150 149 anassrs φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
151 150 expr φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
152 151 ralrimiva φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
153 141 simpld φvordTopSvSr*w*Srwrwvr<S
154 4 ad3antrrr φvordTopSvSr*w*SrwrwvS=suprans𝒫AFinGFs*<
155 153 154 breqtrd φvordTopSvSr*w*Srwrwvr<suprans𝒫AFinGFs*<
156 25 ad3antrrr φvordTopSvSr*w*Srwrwvrans𝒫AFinGFs*
157 supxrlub rans𝒫AFinGFs*r*r<suprans𝒫AFinGFs*<wrans𝒫AFinGFsr<w
158 156 110 157 syl2anc φvordTopSvSr*w*Srwrwvr<suprans𝒫AFinGFs*<wrans𝒫AFinGFsr<w
159 155 158 mpbid φvordTopSvSr*w*Srwrwvwrans𝒫AFinGFsr<w
160 ovex GFzV
161 160 rgenw z𝒫AFinGFzV
162 reseq2 s=zFs=Fz
163 162 oveq2d s=zGFs=GFz
164 163 cbvmptv s𝒫AFinGFs=z𝒫AFinGFz
165 breq2 w=GFzr<wr<GFz
166 164 165 rexrnmptw z𝒫AFinGFzVwrans𝒫AFinGFsr<wz𝒫AFinr<GFz
167 161 166 ax-mp wrans𝒫AFinGFsr<wz𝒫AFinr<GFz
168 159 167 sylib φvordTopSvSr*w*Srwrwvz𝒫AFinr<GFz
169 152 168 reximddv φvordTopSvSr*w*Srwrwvz𝒫AFiny𝒫AFinzyGFyv0+∞
170 169 expr φvordTopSvSr*w*Srwrwvz𝒫AFiny𝒫AFinzyGFyv0+∞
171 eleq2 u=rwSuSrw
172 sseq1 u=rwuvrwv
173 171 172 anbi12d u=rwSuuvSrwrwv
174 173 imbi1d u=rwSuuvz𝒫AFiny𝒫AFinzyGFyv0+∞Srwrwvz𝒫AFiny𝒫AFinzyGFyv0+∞
175 170 174 syl5ibrcom φvordTopSvSr*w*u=rwSuuvz𝒫AFiny𝒫AFinzyGFyv0+∞
176 175 rexlimdvva φvordTopSvSr*w*u=rwSuuvz𝒫AFiny𝒫AFinzyGFyv0+∞
177 87 176 syl5bi φvordTopSvSuran.Suuvz𝒫AFiny𝒫AFinzyGFyv0+∞
178 177 rexlimdv φvordTopSvSuran.Suuvz𝒫AFiny𝒫AFinzyGFyv0+∞
179 83 178 mpd φvordTopSvSz𝒫AFiny𝒫AFinzyGFyv0+∞
180 simplrl φvordTopSvS=+∞vordTop
181 simpr φvordTopSvS=+∞S=+∞
182 simplrr φvordTopSvS=+∞Sv
183 181 182 eqeltrrd φvordTopSvS=+∞+∞v
184 pnfnei vordTop+∞vrr+∞v
185 180 183 184 syl2anc φvordTopSvS=+∞rr+∞v
186 simprr φvordTopSvS=+∞rr+∞vr+∞v
187 186 ad2antrr φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyr+∞v
188 11 a1i φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGCMnd
189 simprl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyy𝒫AFin
190 simp-5l φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyφ
191 190 3 syl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyF:A0+∞
192 99 ad2antrl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyyA
193 191 192 fssresd φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyFy:y0+∞
194 94 ad2antrl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyyFin
195 fvexd φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzy0GV
196 193 194 195 fdmfifsupp φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyfinSupp0GFy
197 8 9 188 189 193 196 gsumcl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFy0+∞
198 5 197 sselid φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFy*
199 rexr rr*
200 199 ad2antrl φvordTopSvS=+∞rr+∞vr*
201 200 ad2antrr φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyr*
202 simplrl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyz𝒫AFin
203 simprr φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyzy
204 203 192 sstrd φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyzA
205 191 204 fssresd φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyFz:z0+∞
206 194 203 116 syl2anc φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyzFin
207 205 206 195 fdmfifsupp φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyfinSupp0GFz
208 8 9 188 202 205 207 gsumcl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFz0+∞
209 5 208 sselid φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFz*
210 simplrr φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyr<GFz
211 190 2 syl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyAV
212 1 211 191 189 203 xrge0gsumle φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFzGFy
213 201 209 198 210 212 xrltletrd φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyr<GFy
214 pnfge GFy*GFy+∞
215 198 214 syl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFy+∞
216 pnfxr +∞*
217 elioc1 r*+∞*GFyr+∞GFy*r<GFyGFy+∞
218 201 216 217 sylancl φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFyr+∞GFy*r<GFyGFy+∞
219 198 213 215 218 mpbir3and φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFyr+∞
220 187 219 sseldd φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFyv
221 220 197 elind φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
222 221 expr φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
223 222 ralrimiva φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFzy𝒫AFinzyGFyv0+∞
224 ltpnf rr<+∞
225 224 ad2antrl φvordTopSvS=+∞rr+∞vr<+∞
226 simplr φvordTopSvS=+∞rr+∞vS=+∞
227 225 226 breqtrrd φvordTopSvS=+∞rr+∞vr<S
228 4 ad3antrrr φvordTopSvS=+∞rr+∞vS=suprans𝒫AFinGFs*<
229 227 228 breqtrd φvordTopSvS=+∞rr+∞vr<suprans𝒫AFinGFs*<
230 25 ad3antrrr φvordTopSvS=+∞rr+∞vrans𝒫AFinGFs*
231 230 200 157 syl2anc φvordTopSvS=+∞rr+∞vr<suprans𝒫AFinGFs*<wrans𝒫AFinGFsr<w
232 229 231 mpbid φvordTopSvS=+∞rr+∞vwrans𝒫AFinGFsr<w
233 232 167 sylib φvordTopSvS=+∞rr+∞vz𝒫AFinr<GFz
234 223 233 reximddv φvordTopSvS=+∞rr+∞vz𝒫AFiny𝒫AFinzyGFyv0+∞
235 185 234 rexlimddv φvordTopSvS=+∞z𝒫AFiny𝒫AFinzyGFyv0+∞
236 ge0nemnf S*0SS−∞
237 28 63 236 syl2anc φS−∞
238 28 237 jca φS*S−∞
239 238 adantr φvordTopSvS*S−∞
240 xrnemnf S*S−∞SS=+∞
241 239 240 sylib φvordTopSvSS=+∞
242 179 235 241 mpjaodan φvordTopSvz𝒫AFiny𝒫AFinzyGFyv0+∞
243 242 expr φvordTopSvz𝒫AFiny𝒫AFinzyGFyv0+∞
244 70 243 syl5 φvordTopSv0+∞z𝒫AFiny𝒫AFinzyGFyv0+∞
245 eleq2 u=v0+∞SuSv0+∞
246 eleq2 u=v0+∞GFyuGFyv0+∞
247 246 imbi2d u=v0+∞zyGFyuzyGFyv0+∞
248 247 rexralbidv u=v0+∞z𝒫AFiny𝒫AFinzyGFyuz𝒫AFiny𝒫AFinzyGFyv0+∞
249 245 248 imbi12d u=v0+∞Suz𝒫AFiny𝒫AFinzyGFyuSv0+∞z𝒫AFiny𝒫AFinzyGFyv0+∞
250 244 249 syl5ibrcom φvordTopu=v0+∞Suz𝒫AFiny𝒫AFinzyGFyu
251 250 rexlimdva φvordTopu=v0+∞Suz𝒫AFiny𝒫AFinzyGFyu
252 69 251 syl5bi φuordTop𝑡0+∞Suz𝒫AFiny𝒫AFinzyGFyu
253 252 ralrimiv φuordTop𝑡0+∞Suz𝒫AFiny𝒫AFinzyGFyu
254 xrstset ordTop=TopSet𝑠*
255 1 254 resstset 0+∞VordTop=TopSetG
256 67 255 ax-mp ordTop=TopSetG
257 8 256 topnval ordTop𝑡0+∞=TopOpenG
258 eqid 𝒫AFin=𝒫AFin
259 11 a1i φGCMnd
260 xrstps 𝑠*TopSp
261 resstps 𝑠*TopSp0+∞V𝑠*𝑠0+∞TopSp
262 260 67 261 mp2an 𝑠*𝑠0+∞TopSp
263 1 262 eqeltri GTopSp
264 263 a1i φGTopSp
265 8 257 258 259 264 2 3 eltsms φSGtsumsFS0+∞uordTop𝑡0+∞Suz𝒫AFiny𝒫AFinzyGFyu
266 65 253 265 mpbir2and φSGtsumsF
267 letsr TosetRel
268 ordthaus TosetRelordTopHaus
269 267 268 mp1i φordTopHaus
270 resthaus ordTopHaus0+∞VordTop𝑡0+∞Haus
271 269 67 270 sylancl φordTop𝑡0+∞Haus
272 8 259 264 2 3 257 271 haustsms2 φSGtsumsFGtsumsF=S
273 266 272 mpd φGtsumsF=S