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 nfcv 
 |-  F/_ x y
9 nfcv 
 |-  F/_ z y
10 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
11 nfcv 
 |-  F/_ x z
12 10 11 nffv 
 |-  F/_ x ( ( x e. A |-> B ) ` z )
13 nfcv 
 |-  F/_ z ( ( x e. A |-> B ) ` x )
14 7 8 9 12 13 cbvsum 
 |-  sum_ z e. y ( ( x e. A |-> B ) ` z ) = sum_ x e. y ( ( x e. A |-> B ) ` x )
15 14 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 ) )
16 nfv 
 |-  F/ x y e. ( ~P A i^i Fin )
17 1 16 nfan 
 |-  F/ x ( ph /\ y e. ( ~P A i^i Fin ) )
18 elpwinss 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
19 18 adantr 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> y C_ A )
20 simpr 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> x e. y )
21 19 20 sseldd 
 |-  ( ( y e. ( ~P A i^i Fin ) /\ x e. y ) -> x e. A )
22 21 adantll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> x e. A )
23 simpll 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ph )
24 23 22 3 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> B e. ( 0 [,) +oo ) )
25 4 fvmpt2 
 |-  ( ( x e. A /\ B e. ( 0 [,) +oo ) ) -> ( ( x e. A |-> B ) ` x ) = B )
26 22 24 25 syl2anc 
 |-  ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ x e. y ) -> ( ( x e. A |-> B ) ` x ) = B )
27 26 ex 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( x e. y -> ( ( x e. A |-> B ) ` x ) = B ) )
28 17 27 ralrimi 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> A. x e. y ( ( x e. A |-> B ) ` x ) = B )
29 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 )
30 28 29 syl 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ x e. y ( ( x e. A |-> B ) ` x ) = sum_ x e. y B )
31 15 30 eqtrd 
 |-  ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> sum_ z e. y ( ( x e. A |-> B ) ` z ) = sum_ x e. y B )
32 31 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 ) )
33 32 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 ) )
34 33 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* , < ) )
35 6 34 eqtrd 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) , RR* , < ) )