Metamath Proof Explorer

Theorem sge0val

Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion sge0val 
|- ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) ) )

Proof

Step Hyp Ref Expression
1 df-sumge0 
 |-  sum^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )
2 1 a1i 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> sum^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) ) )
3 rneq 
 |-  ( x = F -> ran x = ran F )
4 3 eleq2d 
 |-  ( x = F -> ( +oo e. ran x <-> +oo e. ran F ) )
5 4 adantl 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> ( +oo e. ran x <-> +oo e. ran F ) )
6 dmeq 
 |-  ( x = F -> dom x = dom F )
7 6 adantl 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x = F ) -> dom x = dom F )
8 fdm 
 |-  ( F : X --> ( 0 [,] +oo ) -> dom F = X )
9 8 adantr 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x = F ) -> dom F = X )
10 7 9 eqtrd 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x = F ) -> dom x = X )
11 10 pweqd 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x = F ) -> ~P dom x = ~P X )
12 11 ineq1d 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x = F ) -> ( ~P dom x i^i Fin ) = ( ~P X i^i Fin ) )
13 12 mpteq1d 
 |-  ( ( F : X --> ( 0 [,] +oo ) /\ x = F ) -> ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( x ` w ) ) )
14 13 adantll 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( x ` w ) ) )
15 fveq1 
 |-  ( x = F -> ( x ` w ) = ( F ` w ) )
16 15 sumeq2sdv 
 |-  ( x = F -> sum_ w e. y ( x ` w ) = sum_ w e. y ( F ` w ) )
17 16 mpteq2dv 
 |-  ( x = F -> ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( x ` w ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) )
18 17 adantl 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( x ` w ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) )
19 14 18 eqtrd 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) )
20 19 rneqd 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) = ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) )
21 20 supeq1d 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) = sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) )
22 5 21 ifbieq2d 
 |-  ( ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) /\ x = F ) -> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) = if ( +oo e. ran F , +oo , sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) ) )
23 simpr 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> F : X --> ( 0 [,] +oo ) )
24 simpl 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> X e. V )
25 23 24 fexd 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> F e. _V )
26 pnfxr 
 |-  +oo e. RR*
27 26 a1i 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> +oo e. RR* )
28 xrltso 
 |-  < Or RR*
29 28 supex 
 |-  sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) e. _V
30 29 a1i 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) e. _V )
31 27 30 ifexd 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> if ( +oo e. ran F , +oo , sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) ) e. _V )
32 2 22 25 31 fvmptd 
 |-  ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) ) )