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 φ A Fin
sge0iunmptlemfi.b φ x A B V
sge0iunmptlemfi.dj φ Disj x A B
sge0iunmptlemfi.c φ x A k B C 0 +∞
sge0iunmptlemfi.re φ x A sum^ k B C
Assertion sge0iunmptlemfi φ sum^ k x A B C = sum^ x A sum^ k B C

Proof

Step Hyp Ref Expression
1 sge0iunmptlemfi.a φ A Fin
2 sge0iunmptlemfi.b φ x A B V
3 sge0iunmptlemfi.dj φ Disj x A B
4 sge0iunmptlemfi.c φ x A k B C 0 +∞
5 sge0iunmptlemfi.re φ x A sum^ k B C
6 iuneq1 y = x y B = x B
7 6 mpteq1d y = k x y B C = k x B C
8 7 fveq2d y = sum^ k x y B C = sum^ k x B C
9 mpteq1 y = x y sum^ k B C = x sum^ k B C
10 9 fveq2d y = sum^ x y sum^ k B C = sum^ x sum^ k B C
11 8 10 eqeq12d y = sum^ k x y B C = sum^ x y sum^ k B C sum^ k x B C = sum^ x sum^ k B C
12 iuneq1 y = z x y B = x z B
13 12 mpteq1d y = z k x y B C = k x z B C
14 13 fveq2d y = z sum^ k x y B C = sum^ k x z B C
15 mpteq1 y = z x y sum^ k B C = x z sum^ k B C
16 15 fveq2d y = z sum^ x y sum^ k B C = sum^ x z sum^ k B C
17 14 16 eqeq12d y = z sum^ k x y B C = sum^ x y sum^ k B C sum^ k x z B C = sum^ x z sum^ k B C
18 iuneq1 y = z w x y B = x z w B
19 18 mpteq1d y = z w k x y B C = k x z w B C
20 19 fveq2d y = z w sum^ k x y B C = sum^ k x z w B C
21 mpteq1 y = z w x y sum^ k B C = x z w sum^ k B C
22 21 fveq2d y = z w sum^ x y sum^ k B C = sum^ x z w sum^ k B C
23 20 22 eqeq12d y = z w sum^ k x y B C = sum^ x y sum^ k B C sum^ k x z w B C = sum^ x z w sum^ k B C
24 iuneq1 y = A x y B = x A B
25 24 mpteq1d y = A k x y B C = k x A B C
26 25 fveq2d y = A sum^ k x y B C = sum^ k x A B C
27 mpteq1 y = A x y sum^ k B C = x A sum^ k B C
28 27 fveq2d y = A sum^ x y sum^ k B C = sum^ x A sum^ k B C
29 26 28 eqeq12d y = A sum^ k x y B C = sum^ x y sum^ k B C sum^ k x A B C = sum^ x A sum^ k B C
30 0iun x B =
31 mpteq1 x B = k x B C = k C
32 30 31 ax-mp k x B C = k C
33 mpt0 k C =
34 32 33 eqtri k x B C =
35 34 fveq2i sum^ k x B C = sum^
36 mpt0 x sum^ k B C =
37 36 fveq2i sum^ x sum^ k B C = sum^
38 35 37 eqtr4i sum^ k x B C = sum^ x sum^ k B C
39 38 a1i φ sum^ k x B C = sum^ x sum^ k B C
40 nfv x φ z A w A z
41 nfcv _ x sum^
42 nfiu1 _ x x w B
43 nfcv _ x C
44 42 43 nfmpt _ x k x w B C
45 41 44 nffv _ x sum^ k x w B C
46 simprl φ z A w A z z A
47 1 adantr φ z A A Fin
48 simpr φ z A z A
49 ssfi A Fin z A z Fin
50 47 48 49 syl2anc φ z A z Fin
51 46 50 syldan φ z A w A z z Fin
52 simprr φ z A w A z w A z
53 eldifn w A z ¬ w z
54 disjsn z w = ¬ w z
55 53 54 sylibr w A z z w =
56 55 adantl z A w A z z w =
57 56 adantl φ z A w A z z w =
58 57 54 sylib φ z A w A z ¬ w z
59 simpll φ z A x z φ
60 ssel2 z A x z x A
61 60 adantll φ z A x z x A
62 59 61 5 syl2anc φ z A x z sum^ k B C
63 62 recnd φ z A x z sum^ k B C
64 63 adantlrr φ z A w A z x z sum^ k B C
65 csbeq1a x = w B = w / x B
66 nfcsb1v _ x w / x B
67 vex w V
68 66 67 65 iunxsnf x w B = w / x B
69 65 68 eqtr4di x = w B = x w B
70 69 mpteq1d x = w k B C = k x w B C
71 70 fveq2d x = w sum^ k B C = sum^ k x w B C
72 68 mpteq1i k x w B C = k w / x B C
73 72 a1i φ w A z k x w B C = k w / x B C
74 73 fveq2d φ w A z sum^ k x w B C = sum^ k w / x B C
75 eldifi w A z w A
76 nfv x φ w A
77 66 43 nfmpt _ x k w / x B C
78 41 77 nffv _ x sum^ k w / x B C
79 nfcv _ x
80 78 79 nfel x sum^ k w / x B C
81 76 80 nfim x φ w A sum^ k w / x B C
82 eleq1w x = w x A w A
83 82 anbi2d x = w φ x A φ w A
84 70 72 eqtrdi x = w k B C = k w / x B C
85 84 fveq2d x = w sum^ k B C = sum^ k w / x B C
86 85 eleq1d x = w sum^ k B C sum^ k w / x B C
87 83 86 imbi12d x = w φ x A sum^ k B C φ w A sum^ k w / x B C
88 81 87 5 chvarfv φ w A sum^ k w / x B C
89 75 88 sylan2 φ w A z sum^ k w / x B C
90 74 89 eqeltrd φ w A z sum^ k x w B C
91 90 adantrl φ z A w A z sum^ k x w B C
92 91 recnd φ z A w A z sum^ k x w B C
93 40 45 51 52 58 64 71 92 fsumsplitsn φ z A w A z x z w sum^ k B C = x z sum^ k B C + sum^ k x w B C
94 93 eqcomd φ z A w A z x z sum^ k B C + sum^ k x w B C = x z w sum^ k B C
95 94 adantr φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C x z sum^ k B C + sum^ k x w B C = x z w sum^ k B C
96 iunxun x z w B = x z B x w B
97 96 mpteq1i k x z w B C = k x z B x w B C
98 97 fveq2i sum^ k x z w B C = sum^ k x z B x w B C
99 98 a1i φ z A w A z sum^ k x z w B C = sum^ k x z B x w B C
100 nfv k φ z A w A z
101 2 ralrimiva φ x A B V
102 iunexg A Fin x A B V x A B V
103 1 101 102 syl2anc φ x A B V
104 103 adantr φ z A x A B V
105 iunss1 z A x z B x A B
106 105 adantl φ z A x z B x A B
107 104 106 ssexd φ z A x z B V
108 107 adantrr φ z A w A z x z B V
109 103 adantr φ w A z x A B V
110 snssi w A w A
111 75 110 syl w A z w A
112 iunss1 w A x w B x A B
113 111 112 syl w A z x w B x A B
114 113 adantl φ w A z x w B x A B
115 109 114 ssexd φ w A z x w B V
116 115 adantrl φ z A w A z x w B V
117 3 adantr φ z A w A z Disj x A B
118 111 ad2antll φ z A w A z w A
119 disjiun Disj x A B z A w A z w = x z B x w B =
120 117 46 118 57 119 syl13anc φ z A w A z x z B x w B =
121 eliun k x z B x z k B
122 121 biimpi k x z B x z k B
123 122 adantl φ z A k x z B x z k B
124 simp1l φ z A x z k B φ
125 61 3adant3 φ z A x z k B x A
126 simp3 φ z A x z k B k B
127 124 125 126 4 syl3anc φ z A x z k B C 0 +∞
128 127 3exp φ z A x z k B C 0 +∞
129 128 rexlimdv φ z A x z k B C 0 +∞
130 129 adantr φ z A k x z B x z k B C 0 +∞
131 123 130 mpd φ z A k x z B C 0 +∞
132 131 adantlrr φ z A w A z k x z B C 0 +∞
133 eliun k x w B x w k B
134 133 biimpi k x w B x w k B
135 134 adantl φ w A z k x w B x w k B
136 simp1l φ w A z x w k B φ
137 111 sselda w A z x w x A
138 137 adantll φ w A z x w x A
139 138 3adant3 φ w A z x w k B x A
140 simp3 φ w A z x w k B k B
141 136 139 140 4 syl3anc φ w A z x w k B C 0 +∞
142 141 3exp φ w A z x w k B C 0 +∞
143 142 rexlimdv φ w A z x w k B C 0 +∞
144 143 adantr φ w A z k x w B x w k B C 0 +∞
145 135 144 mpd φ w A z k x w B C 0 +∞
146 145 adantlrl φ z A w A z k x w B C 0 +∞
147 100 108 116 120 132 146 sge0splitmpt φ z A w A z sum^ k x z B x w B C = sum^ k x z B C + 𝑒 sum^ k x w B C
148 99 147 eqtrd φ z A w A z sum^ k x z w B C = sum^ k x z B C + 𝑒 sum^ k x w B C
149 148 adantr φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z w B C = sum^ k x z B C + 𝑒 sum^ k x w B C
150 id sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z B C = sum^ x z sum^ k B C
151 150 adantl φ z A sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z B C = sum^ x z sum^ k B C
152 4 3expa φ x A k B C 0 +∞
153 eqid k B C = k B C
154 152 153 fmptd φ x A k B C : B 0 +∞
155 2 154 sge0ge0 φ x A 0 sum^ k B C
156 5 155 jca φ x A sum^ k B C 0 sum^ k B C
157 elrege0 sum^ k B C 0 +∞ sum^ k B C 0 sum^ k B C
158 156 157 sylibr φ x A sum^ k B C 0 +∞
159 59 61 158 syl2anc φ z A x z sum^ k B C 0 +∞
160 eqid x z sum^ k B C = x z sum^ k B C
161 159 160 fmptd φ z A x z sum^ k B C : z 0 +∞
162 50 161 sge0fsum φ z A sum^ x z sum^ k B C = y z x z sum^ k B C y
163 162 adantr φ z A sum^ k x z B C = sum^ x z sum^ k B C sum^ x z sum^ k B C = y z x z sum^ k B C y
164 fveq2 y = x x z sum^ k B C y = x z sum^ k B C x
165 nfcv _ x z
166 nfcv _ y z
167 nfmpt1 _ x x z sum^ k B C
168 nfcv _ x y
169 167 168 nffv _ x x z sum^ k B C y
170 nfcv _ y x z sum^ k B C x
171 164 165 166 169 170 cbvsum y z x z sum^ k B C y = x z x z sum^ k B C x
172 171 a1i φ z A y z x z sum^ k B C y = x z x z sum^ k B C x
173 id x z x z
174 fvexd x z sum^ k B C V
175 160 fvmpt2 x z sum^ k B C V x z sum^ k B C x = sum^ k B C
176 173 174 175 syl2anc x z x z sum^ k B C x = sum^ k B C
177 176 adantl φ z A x z x z sum^ k B C x = sum^ k B C
178 177 ralrimiva φ z A x z x z sum^ k B C x = sum^ k B C
179 178 sumeq2d φ z A x z x z sum^ k B C x = x z sum^ k B C
180 172 179 eqtrd φ z A y z x z sum^ k B C y = x z sum^ k B C
181 180 adantr φ z A sum^ k x z B C = sum^ x z sum^ k B C y z x z sum^ k B C y = x z sum^ k B C
182 151 163 181 3eqtrd φ z A sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z B C = x z sum^ k B C
183 182 adantlrr φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z B C = x z sum^ k B C
184 183 oveq1d φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z B C + 𝑒 sum^ k x w B C = x z sum^ k B C + 𝑒 sum^ k x w B C
185 50 62 fsumrecl φ z A x z sum^ k B C
186 185 adantrr φ z A w A z x z sum^ k B C
187 rexadd x z sum^ k B C sum^ k x w B C x z sum^ k B C + 𝑒 sum^ k x w B C = x z sum^ k B C + sum^ k x w B C
188 186 91 187 syl2anc φ z A w A z x z sum^ k B C + 𝑒 sum^ k x w B C = x z sum^ k B C + sum^ k x w B C
189 188 adantr φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C x z sum^ k B C + 𝑒 sum^ k x w B C = x z sum^ k B C + sum^ k x w B C
190 149 184 189 3eqtrd φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z w B C = x z sum^ k B C + sum^ k x w B C
191 snfi w Fin
192 191 a1i φ z A w A z w Fin
193 unfi z Fin w Fin z w Fin
194 51 192 193 syl2anc φ z A w A z z w Fin
195 simpll φ z A w A z x z w φ
196 60 ad4ant14 z A w A z x z w x z x A
197 simpll w A z x z w ¬ x z w A z
198 elunnel1 x z w ¬ x z x w
199 elsni x w x = w
200 198 199 syl x z w ¬ x z x = w
201 200 adantll w A z x z w ¬ x z x = w
202 simpr w A z x = w x = w
203 75 adantr w A z x = w w A
204 202 203 eqeltrd w A z x = w x A
205 197 201 204 syl2anc w A z x z w ¬ x z x A
206 205 adantlll z A w A z x z w ¬ x z x A
207 196 206 pm2.61dan z A w A z x z w x A
208 207 adantll φ z A w A z x z w x A
209 195 208 158 syl2anc φ z A w A z x z w sum^ k B C 0 +∞
210 194 209 sge0fsummpt φ z A w A z sum^ x z w sum^ k B C = x z w sum^ k B C
211 210 adantr φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ x z w sum^ k B C = x z w sum^ k B C
212 95 190 211 3eqtr4d φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z w B C = sum^ x z w sum^ k B C
213 212 ex φ z A w A z sum^ k x z B C = sum^ x z sum^ k B C sum^ k x z w B C = sum^ x z w sum^ k B C
214 11 17 23 29 39 213 1 findcard2d φ sum^ k x A B C = sum^ x A sum^ k B C