Metamath Proof Explorer

Theorem fsumlesge0

Description: Every finite subsum of nonnegative reals is less than or equal to the extended sum over the whole (possibly infinite) domain. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fsumlesge0.x 
|- ( ph -> X e. V )
fsumlesge0.f 
|- ( ph -> F : X --> ( 0 [,) +oo ) )
fsumlesge0.y 
|- ( ph -> Y C_ X )
fsumlesge0.fi 
|- ( ph -> Y e. Fin )
Assertion fsumlesge0 
|- ( ph -> sum_ x e. Y ( F ` x ) <_ ( sum^ ` F ) )

Proof

Step Hyp Ref Expression
1 fsumlesge0.x 
 |-  ( ph -> X e. V )
2 fsumlesge0.f 
 |-  ( ph -> F : X --> ( 0 [,) +oo ) )
3 fsumlesge0.y 
 |-  ( ph -> Y C_ X )
4 fsumlesge0.fi 
 |-  ( ph -> Y e. Fin )
5 2 sge0rnre 
 |-  ( ph -> ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) C_ RR )
6 ressxr 
 |-  RR C_ RR*
7 6 a1i 
 |-  ( ph -> RR C_ RR* )
8 5 7 sstrd 
 |-  ( ph -> ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) C_ RR* )
9 1 3 ssexd 
 |-  ( ph -> Y e. _V )
10 elpwg 
 |-  ( Y e. _V -> ( Y e. ~P X <-> Y C_ X ) )
11 9 10 syl 
 |-  ( ph -> ( Y e. ~P X <-> Y C_ X ) )
12 3 11 mpbird 
 |-  ( ph -> Y e. ~P X )
13 12 4 elind 
 |-  ( ph -> Y e. ( ~P X i^i Fin ) )
14 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
15 14 cbvsumv 
 |-  sum_ x e. Y ( F ` x ) = sum_ z e. Y ( F ` z )
16 15 a1i 
 |-  ( ph -> sum_ x e. Y ( F ` x ) = sum_ z e. Y ( F ` z ) )
17 sumeq1 
 |-  ( y = Y -> sum_ z e. y ( F ` z ) = sum_ z e. Y ( F ` z ) )
18 17 rspceeqv 
 |-  ( ( Y e. ( ~P X i^i Fin ) /\ sum_ x e. Y ( F ` x ) = sum_ z e. Y ( F ` z ) ) -> E. y e. ( ~P X i^i Fin ) sum_ x e. Y ( F ` x ) = sum_ z e. y ( F ` z ) )
19 13 16 18 syl2anc 
 |-  ( ph -> E. y e. ( ~P X i^i Fin ) sum_ x e. Y ( F ` x ) = sum_ z e. y ( F ` z ) )
20 sumex 
 |-  sum_ x e. Y ( F ` x ) e. _V
21 20 a1i 
 |-  ( ph -> sum_ x e. Y ( F ` x ) e. _V )
22 eqid 
 |-  ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) )
23 22 elrnmpt 
 |-  ( sum_ x e. Y ( F ` x ) e. _V -> ( sum_ x e. Y ( F ` x ) e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) <-> E. y e. ( ~P X i^i Fin ) sum_ x e. Y ( F ` x ) = sum_ z e. y ( F ` z ) ) )
24 21 23 syl 
 |-  ( ph -> ( sum_ x e. Y ( F ` x ) e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) <-> E. y e. ( ~P X i^i Fin ) sum_ x e. Y ( F ` x ) = sum_ z e. y ( F ` z ) ) )
25 19 24 mpbird 
 |-  ( ph -> sum_ x e. Y ( F ` x ) e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) )
26 supxrub 
 |-  ( ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) C_ RR* /\ sum_ x e. Y ( F ` x ) e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) ) -> sum_ x e. Y ( F ` x ) <_ sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) , RR* , < ) )
27 8 25 26 syl2anc 
 |-  ( ph -> sum_ x e. Y ( F ` x ) <_ sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) , RR* , < ) )
28 1 2 sge0reval 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) , RR* , < ) )
29 28 eqcomd 
 |-  ( ph -> sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ z e. y ( F ` z ) ) , RR* , < ) = ( sum^ ` F ) )
30 27 29 breqtrd 
 |-  ( ph -> sum_ x e. Y ( F ` x ) <_ ( sum^ ` F ) )