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 
|- ( ph -> A e. V )
sge0iun.b 
|- ( ( ph /\ x e. A ) -> B e. W )
sge0iun.x 
|- X = U_ x e. A B
sge0iun.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0iun.dj 
|- ( ph -> Disj_ x e. A B )
Assertion sge0iun 
|- ( ph -> ( sum^ ` F ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( F |` B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sge0iun.a 
 |-  ( ph -> A e. V )
2 sge0iun.b 
 |-  ( ( ph /\ x e. A ) -> B e. W )
3 sge0iun.x 
 |-  X = U_ x e. A B
4 sge0iun.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
5 sge0iun.dj 
 |-  ( ph -> Disj_ x e. A B )
6 4 adantr 
 |-  ( ( ph /\ x e. A ) -> F : X --> ( 0 [,] +oo ) )
7 6 3adant3 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> F : X --> ( 0 [,] +oo ) )
8 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
9 8 adantl 
 |-  ( ( ph /\ x e. A ) -> B C_ U_ x e. A B )
10 3 eqcomi 
 |-  U_ x e. A B = X
11 9 10 sseqtrdi 
 |-  ( ( ph /\ x e. A ) -> B C_ X )
12 11 3adant3 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> B C_ X )
13 simp3 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> y e. B )
14 12 13 sseldd 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> y e. X )
15 7 14 ffvelcdmd 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> ( F ` y ) e. ( 0 [,] +oo ) )
16 1 2 5 15 sge0iunmpt 
 |-  ( ph -> ( sum^ ` ( y e. U_ x e. A B |-> ( F ` y ) ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( y e. B |-> ( F ` y ) ) ) ) ) )
17 3 feq2i 
 |-  ( F : X --> ( 0 [,] +oo ) <-> F : U_ x e. A B --> ( 0 [,] +oo ) )
18 17 a1i 
 |-  ( ph -> ( F : X --> ( 0 [,] +oo ) <-> F : U_ x e. A B --> ( 0 [,] +oo ) ) )
19 4 18 mpbid 
 |-  ( ph -> F : U_ x e. A B --> ( 0 [,] +oo ) )
20 19 feqmptd 
 |-  ( ph -> F = ( y e. U_ x e. A B |-> ( F ` y ) ) )
21 20 fveq2d 
 |-  ( ph -> ( sum^ ` F ) = ( sum^ ` ( y e. U_ x e. A B |-> ( F ` y ) ) ) )
22 6 11 fssresd 
 |-  ( ( ph /\ x e. A ) -> ( F |` B ) : B --> ( 0 [,] +oo ) )
23 22 feqmptd 
 |-  ( ( ph /\ x e. A ) -> ( F |` B ) = ( y e. B |-> ( ( F |` B ) ` y ) ) )
24 fvres 
 |-  ( y e. B -> ( ( F |` B ) ` y ) = ( F ` y ) )
25 24 mpteq2ia 
 |-  ( y e. B |-> ( ( F |` B ) ` y ) ) = ( y e. B |-> ( F ` y ) )
26 25 a1i 
 |-  ( ( ph /\ x e. A ) -> ( y e. B |-> ( ( F |` B ) ` y ) ) = ( y e. B |-> ( F ` y ) ) )
27 23 26 eqtrd 
 |-  ( ( ph /\ x e. A ) -> ( F |` B ) = ( y e. B |-> ( F ` y ) ) )
28 27 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( sum^ ` ( F |` B ) ) = ( sum^ ` ( y e. B |-> ( F ` y ) ) ) )
29 28 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( sum^ ` ( F |` B ) ) ) = ( x e. A |-> ( sum^ ` ( y e. B |-> ( F ` y ) ) ) ) )
30 29 fveq2d 
 |-  ( ph -> ( sum^ ` ( x e. A |-> ( sum^ ` ( F |` B ) ) ) ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( y e. B |-> ( F ` y ) ) ) ) ) )
31 16 21 30 3eqtr4d 
 |-  ( ph -> ( sum^ ` F ) = ( sum^ ` ( x e. A |-> ( sum^ ` ( F |` B ) ) ) ) )