Metamath Proof Explorer


Theorem sge0iunmptlemfi

Description: Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iunmptlemfi.a φAFin
sge0iunmptlemfi.b φxABV
sge0iunmptlemfi.dj φDisjxAB
sge0iunmptlemfi.c φxAkBC0+∞
sge0iunmptlemfi.re φxAsum^kBC
Assertion sge0iunmptlemfi φsum^kxABC=sum^xAsum^kBC

Proof

Step Hyp Ref Expression
1 sge0iunmptlemfi.a φAFin
2 sge0iunmptlemfi.b φxABV
3 sge0iunmptlemfi.dj φDisjxAB
4 sge0iunmptlemfi.c φxAkBC0+∞
5 sge0iunmptlemfi.re φxAsum^kBC
6 iuneq1 y=xyB=xB
7 6 mpteq1d y=kxyBC=kxBC
8 7 fveq2d y=sum^kxyBC=sum^kxBC
9 mpteq1 y=xysum^kBC=xsum^kBC
10 9 fveq2d y=sum^xysum^kBC=sum^xsum^kBC
11 8 10 eqeq12d y=sum^kxyBC=sum^xysum^kBCsum^kxBC=sum^xsum^kBC
12 iuneq1 y=zxyB=xzB
13 12 mpteq1d y=zkxyBC=kxzBC
14 13 fveq2d y=zsum^kxyBC=sum^kxzBC
15 mpteq1 y=zxysum^kBC=xzsum^kBC
16 15 fveq2d y=zsum^xysum^kBC=sum^xzsum^kBC
17 14 16 eqeq12d y=zsum^kxyBC=sum^xysum^kBCsum^kxzBC=sum^xzsum^kBC
18 iuneq1 y=zwxyB=xzwB
19 18 mpteq1d y=zwkxyBC=kxzwBC
20 19 fveq2d y=zwsum^kxyBC=sum^kxzwBC
21 mpteq1 y=zwxysum^kBC=xzwsum^kBC
22 21 fveq2d y=zwsum^xysum^kBC=sum^xzwsum^kBC
23 20 22 eqeq12d y=zwsum^kxyBC=sum^xysum^kBCsum^kxzwBC=sum^xzwsum^kBC
24 iuneq1 y=AxyB=xAB
25 24 mpteq1d y=AkxyBC=kxABC
26 25 fveq2d y=Asum^kxyBC=sum^kxABC
27 mpteq1 y=Axysum^kBC=xAsum^kBC
28 27 fveq2d y=Asum^xysum^kBC=sum^xAsum^kBC
29 26 28 eqeq12d y=Asum^kxyBC=sum^xysum^kBCsum^kxABC=sum^xAsum^kBC
30 0iun xB=
31 mpteq1 xB=kxBC=kC
32 30 31 ax-mp kxBC=kC
33 mpt0 kC=
34 32 33 eqtri kxBC=
35 34 fveq2i sum^kxBC=sum^
36 mpt0 xsum^kBC=
37 36 fveq2i sum^xsum^kBC=sum^
38 35 37 eqtr4i sum^kxBC=sum^xsum^kBC
39 38 a1i φsum^kxBC=sum^xsum^kBC
40 nfv xφzAwAz
41 nfcv _xsum^
42 nfiu1 _xxwB
43 nfcv _xC
44 42 43 nfmpt _xkxwBC
45 41 44 nffv _xsum^kxwBC
46 simprl φzAwAzzA
47 1 adantr φzAAFin
48 simpr φzAzA
49 ssfi AFinzAzFin
50 47 48 49 syl2anc φzAzFin
51 46 50 syldan φzAwAzzFin
52 simprr φzAwAzwAz
53 eldifn wAz¬wz
54 disjsn zw=¬wz
55 53 54 sylibr wAzzw=
56 55 adantl zAwAzzw=
57 56 adantl φzAwAzzw=
58 57 54 sylib φzAwAz¬wz
59 simpll φzAxzφ
60 ssel2 zAxzxA
61 60 adantll φzAxzxA
62 59 61 5 syl2anc φzAxzsum^kBC
63 62 recnd φzAxzsum^kBC
64 63 adantlrr φzAwAzxzsum^kBC
65 csbeq1a x=wB=w/xB
66 nfcsb1v _xw/xB
67 vex wV
68 66 67 65 iunxsnf xwB=w/xB
69 65 68 eqtr4di x=wB=xwB
70 69 mpteq1d x=wkBC=kxwBC
71 70 fveq2d x=wsum^kBC=sum^kxwBC
72 68 mpteq1i kxwBC=kw/xBC
73 72 a1i φwAzkxwBC=kw/xBC
74 73 fveq2d φwAzsum^kxwBC=sum^kw/xBC
75 eldifi wAzwA
76 nfv xφwA
77 66 43 nfmpt _xkw/xBC
78 41 77 nffv _xsum^kw/xBC
79 nfcv _x
80 78 79 nfel xsum^kw/xBC
81 76 80 nfim xφwAsum^kw/xBC
82 eleq1w x=wxAwA
83 82 anbi2d x=wφxAφwA
84 70 72 eqtrdi x=wkBC=kw/xBC
85 84 fveq2d x=wsum^kBC=sum^kw/xBC
86 85 eleq1d x=wsum^kBCsum^kw/xBC
87 83 86 imbi12d x=wφxAsum^kBCφwAsum^kw/xBC
88 81 87 5 chvarfv φwAsum^kw/xBC
89 75 88 sylan2 φwAzsum^kw/xBC
90 74 89 eqeltrd φwAzsum^kxwBC
91 90 adantrl φzAwAzsum^kxwBC
92 91 recnd φzAwAzsum^kxwBC
93 40 45 51 52 58 64 71 92 fsumsplitsn φzAwAzxzwsum^kBC=xzsum^kBC+sum^kxwBC
94 93 eqcomd φzAwAzxzsum^kBC+sum^kxwBC=xzwsum^kBC
95 94 adantr φzAwAzsum^kxzBC=sum^xzsum^kBCxzsum^kBC+sum^kxwBC=xzwsum^kBC
96 iunxun xzwB=xzBxwB
97 96 mpteq1i kxzwBC=kxzBxwBC
98 97 fveq2i sum^kxzwBC=sum^kxzBxwBC
99 98 a1i φzAwAzsum^kxzwBC=sum^kxzBxwBC
100 nfv kφzAwAz
101 2 ralrimiva φxABV
102 iunexg AFinxABVxABV
103 1 101 102 syl2anc φxABV
104 103 adantr φzAxABV
105 iunss1 zAxzBxAB
106 105 adantl φzAxzBxAB
107 104 106 ssexd φzAxzBV
108 107 adantrr φzAwAzxzBV
109 103 adantr φwAzxABV
110 snssi wAwA
111 75 110 syl wAzwA
112 iunss1 wAxwBxAB
113 111 112 syl wAzxwBxAB
114 113 adantl φwAzxwBxAB
115 109 114 ssexd φwAzxwBV
116 115 adantrl φzAwAzxwBV
117 3 adantr φzAwAzDisjxAB
118 111 ad2antll φzAwAzwA
119 disjiun DisjxABzAwAzw=xzBxwB=
120 117 46 118 57 119 syl13anc φzAwAzxzBxwB=
121 eliun kxzBxzkB
122 121 biimpi kxzBxzkB
123 122 adantl φzAkxzBxzkB
124 simp1l φzAxzkBφ
125 61 3adant3 φzAxzkBxA
126 simp3 φzAxzkBkB
127 124 125 126 4 syl3anc φzAxzkBC0+∞
128 127 3exp φzAxzkBC0+∞
129 128 rexlimdv φzAxzkBC0+∞
130 129 adantr φzAkxzBxzkBC0+∞
131 123 130 mpd φzAkxzBC0+∞
132 131 adantlrr φzAwAzkxzBC0+∞
133 eliun kxwBxwkB
134 133 biimpi kxwBxwkB
135 134 adantl φwAzkxwBxwkB
136 simp1l φwAzxwkBφ
137 111 sselda wAzxwxA
138 137 adantll φwAzxwxA
139 138 3adant3 φwAzxwkBxA
140 simp3 φwAzxwkBkB
141 136 139 140 4 syl3anc φwAzxwkBC0+∞
142 141 3exp φwAzxwkBC0+∞
143 142 rexlimdv φwAzxwkBC0+∞
144 143 adantr φwAzkxwBxwkBC0+∞
145 135 144 mpd φwAzkxwBC0+∞
146 145 adantlrl φzAwAzkxwBC0+∞
147 100 108 116 120 132 146 sge0splitmpt φzAwAzsum^kxzBxwBC=sum^kxzBC+𝑒sum^kxwBC
148 99 147 eqtrd φzAwAzsum^kxzwBC=sum^kxzBC+𝑒sum^kxwBC
149 148 adantr φzAwAzsum^kxzBC=sum^xzsum^kBCsum^kxzwBC=sum^kxzBC+𝑒sum^kxwBC
150 id sum^kxzBC=sum^xzsum^kBCsum^kxzBC=sum^xzsum^kBC
151 150 adantl φzAsum^kxzBC=sum^xzsum^kBCsum^kxzBC=sum^xzsum^kBC
152 4 3expa φxAkBC0+∞
153 eqid kBC=kBC
154 152 153 fmptd φxAkBC:B0+∞
155 2 154 sge0ge0 φxA0sum^kBC
156 5 155 jca φxAsum^kBC0sum^kBC
157 elrege0 sum^kBC0+∞sum^kBC0sum^kBC
158 156 157 sylibr φxAsum^kBC0+∞
159 59 61 158 syl2anc φzAxzsum^kBC0+∞
160 eqid xzsum^kBC=xzsum^kBC
161 159 160 fmptd φzAxzsum^kBC:z0+∞
162 50 161 sge0fsum φzAsum^xzsum^kBC=yzxzsum^kBCy
163 162 adantr φzAsum^kxzBC=sum^xzsum^kBCsum^xzsum^kBC=yzxzsum^kBCy
164 fveq2 y=xxzsum^kBCy=xzsum^kBCx
165 nfcv _xz
166 nfcv _yz
167 nfmpt1 _xxzsum^kBC
168 nfcv _xy
169 167 168 nffv _xxzsum^kBCy
170 nfcv _yxzsum^kBCx
171 164 165 166 169 170 cbvsum yzxzsum^kBCy=xzxzsum^kBCx
172 171 a1i φzAyzxzsum^kBCy=xzxzsum^kBCx
173 id xzxz
174 fvexd xzsum^kBCV
175 160 fvmpt2 xzsum^kBCVxzsum^kBCx=sum^kBC
176 173 174 175 syl2anc xzxzsum^kBCx=sum^kBC
177 176 adantl φzAxzxzsum^kBCx=sum^kBC
178 177 ralrimiva φzAxzxzsum^kBCx=sum^kBC
179 178 sumeq2d φzAxzxzsum^kBCx=xzsum^kBC
180 172 179 eqtrd φzAyzxzsum^kBCy=xzsum^kBC
181 180 adantr φzAsum^kxzBC=sum^xzsum^kBCyzxzsum^kBCy=xzsum^kBC
182 151 163 181 3eqtrd φzAsum^kxzBC=sum^xzsum^kBCsum^kxzBC=xzsum^kBC
183 182 adantlrr φzAwAzsum^kxzBC=sum^xzsum^kBCsum^kxzBC=xzsum^kBC
184 183 oveq1d φzAwAzsum^kxzBC=sum^xzsum^kBCsum^kxzBC+𝑒sum^kxwBC=xzsum^kBC+𝑒sum^kxwBC
185 50 62 fsumrecl φzAxzsum^kBC
186 185 adantrr φzAwAzxzsum^kBC
187 rexadd xzsum^kBCsum^kxwBCxzsum^kBC+𝑒sum^kxwBC=xzsum^kBC+sum^kxwBC
188 186 91 187 syl2anc φzAwAzxzsum^kBC+𝑒sum^kxwBC=xzsum^kBC+sum^kxwBC
189 188 adantr φzAwAzsum^kxzBC=sum^xzsum^kBCxzsum^kBC+𝑒sum^kxwBC=xzsum^kBC+sum^kxwBC
190 149 184 189 3eqtrd φzAwAzsum^kxzBC=sum^xzsum^kBCsum^kxzwBC=xzsum^kBC+sum^kxwBC
191 snfi wFin
192 191 a1i φzAwAzwFin
193 unfi zFinwFinzwFin
194 51 192 193 syl2anc φzAwAzzwFin
195 simpll φzAwAzxzwφ
196 60 ad4ant14 zAwAzxzwxzxA
197 simpll wAzxzw¬xzwAz
198 elunnel1 xzw¬xzxw
199 elsni xwx=w
200 198 199 syl xzw¬xzx=w
201 200 adantll wAzxzw¬xzx=w
202 simpr wAzx=wx=w
203 75 adantr wAzx=wwA
204 202 203 eqeltrd wAzx=wxA
205 197 201 204 syl2anc wAzxzw¬xzxA
206 205 adantlll zAwAzxzw¬xzxA
207 196 206 pm2.61dan zAwAzxzwxA
208 207 adantll φzAwAzxzwxA
209 195 208 158 syl2anc φzAwAzxzwsum^kBC0+∞
210 194 209 sge0fsummpt φzAwAzsum^xzwsum^kBC=xzwsum^kBC
211 210 adantr φzAwAzsum^kxzBC=sum^xzsum^kBCsum^xzwsum^kBC=xzwsum^kBC
212 95 190 211 3eqtr4d φzAwAzsum^kxzBC=sum^xzsum^kBCsum^kxzwBC=sum^xzwsum^kBC
213 212 ex φzAwAzsum^kxzBC=sum^xzsum^kBCsum^kxzwBC=sum^xzwsum^kBC
214 11 17 23 29 39 213 1 findcard2d φsum^kxABC=sum^xAsum^kBC