Metamath Proof Explorer

Theorem sge0revalmpt

Description: Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0revalmpt.1 
|- F/ x ph
sge0revalmpt.2 
|- ( ph -> A e. V )
sge0revalmpt.3 
|- ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
Assertion sge0revalmpt 
|- ( ph -> ( sum^ ` ( x e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 sge0revalmpt.1 
 |-  F/ x ph
2 sge0revalmpt.2 
 |-  ( ph -> A e. V )
3 sge0revalmpt.3 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
4 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
5 1 3 4 fmptdf 
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,) +oo ) )
6 2 5 sge0reval 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ z e. y ( ( x e. A |-> B ) ` z ) ) , RR* , < ) )
7 fveq2 
 |-  ( z = x -> ( ( x e. A |-> B ) ` z ) = ( ( x e. A |-> B ) ` x ) )
8 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
9 nfcv 
 |-  F/_ x z
10 8 9 nffv 
 |-  F/_ x ( ( x e. A |-> B ) ` z )
11 nfcv 
 |-  F/_ z ( ( x e. A |-> B ) ` x )
12 7 10 11 cbvsum 
 |-  sum_ z e. y ( ( x e. A |-> B ) ` z ) = sum_ x e. y ( ( x e. A |-> B ) ` x )
13 12 a1i 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ z e. y ( ( x e. A |-> B ) ` z ) = sum_ x e. y ( ( x e. A |-> B ) ` x ) )
14 nfv 
 |-  F/ x y e. ( ~P A i^i Fin )
15 1 14 nfan 
 |-  F/ x ( ph /\ y e. ( ~P A i^i Fin ) )
16 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
17 16 adantr 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> y C_ A )
18 simpr 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> x e. y )
19 17 18 sseldd 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> x e. A )
20 19 adantll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> x e. A )
21 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ph )
22 21 20 3 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> B e. ( 0 [,) +oo ) )
23 4 fvmpt2 
 |-  ( ( x e. A /\ B e. ( 0 [,) +oo ) ) -> ( ( x e. A |-> B ) ` x ) = B )
24 20 22 23 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( ( x e. A |-> B ) ` x ) = B )
25 24 ex 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( x e. y -> ( ( x e. A |-> B ) ` x ) = B ) )
26 15 25 ralrimi 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> A. x e. y ( ( x e. A |-> B ) ` x ) = B )
27 sumeq2 
 |-  ( A. x e. y ( ( x e. A |-> B ) ` x ) = B -> sum_ x e. y ( ( x e. A |-> B ) ` x ) = sum_ x e. y B )
28 26 27 syl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ x e. y ( ( x e. A |-> B ) ` x ) = sum_ x e. y B )
29 13 28 eqtrd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ z e. y ( ( x e. A |-> B ) ` z ) = sum_ x e. y B )
30 29 mpteq2dva 
 |-  ( ph -> ( y e. ( ~P A i^i Fin ) |-> sum_ z e. y ( ( x e. A |-> B ) ` z ) ) = ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) )
31 30 rneqd 
 |-  ( ph -> ran ( y e. ( ~P A i^i Fin ) |-> sum_ z e. y ( ( x e. A |-> B ) ` z ) ) = ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) )
32 31 supeq1d 
 |-  ( ph -> sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ z e. y ( ( x e. A |-> B ) ` z ) ) , RR* , < ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) , RR* , < ) )
33 6 32 eqtrd 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) , RR* , < ) )