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 ffvelrnd
 |-  ( ( 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 ) ) ) ) )