Metamath Proof Explorer


Theorem sge0iun

Description: Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0iun.a φ A V
sge0iun.b φ x A B W
sge0iun.x X = x A B
sge0iun.f φ F : X 0 +∞
sge0iun.dj φ Disj x A B
Assertion sge0iun φ sum^ F = sum^ x A sum^ F B

Proof

Step Hyp Ref Expression
1 sge0iun.a φ A V
2 sge0iun.b φ x A B W
3 sge0iun.x X = x A B
4 sge0iun.f φ F : X 0 +∞
5 sge0iun.dj φ Disj x A B
6 4 adantr φ x A F : X 0 +∞
7 6 3adant3 φ x A y B F : X 0 +∞
8 ssiun2 x A B x A B
9 8 adantl φ x A B x A B
10 3 eqcomi x A B = X
11 9 10 sseqtrdi φ x A B X
12 11 3adant3 φ x A y B B X
13 simp3 φ x A y B y B
14 12 13 sseldd φ x A y B y X
15 7 14 ffvelrnd φ x A y B F y 0 +∞
16 1 2 5 15 sge0iunmpt φ sum^ y x A B F y = sum^ x A sum^ y B F y
17 3 feq2i F : X 0 +∞ F : x A B 0 +∞
18 17 a1i φ F : X 0 +∞ F : x A B 0 +∞
19 4 18 mpbid φ F : x A B 0 +∞
20 19 feqmptd φ F = y x A B F y
21 20 fveq2d φ sum^ F = sum^ y x A B F y
22 6 11 fssresd φ x A F B : B 0 +∞
23 22 feqmptd φ x A F B = y B F B y
24 fvres y B F B y = F y
25 24 mpteq2ia y B F B y = y B F y
26 25 a1i φ x A y B F B y = y B F y
27 23 26 eqtrd φ x A F B = y B F y
28 27 fveq2d φ x A sum^ F B = sum^ y B F y
29 28 mpteq2dva φ x A sum^ F B = x A sum^ y B F y
30 29 fveq2d φ sum^ x A sum^ F B = sum^ x A sum^ y B F y
31 16 21 30 3eqtr4d φ sum^ F = sum^ x A sum^ F B