Metamath Proof Explorer

Theorem sge0less

Description: A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0less.1 
|- ( ph -> X e. V )
sge0less.2 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
Assertion sge0less 
|- ( ph -> ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) )

Proof

Step Hyp Ref Expression
1 sge0less.1 
 |-  ( ph -> X e. V )
2 sge0less.2 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 inex1g 
 |-  ( X e. V -> ( X i^i Y ) e. _V )
4 1 3 syl 
 |-  ( ph -> ( X i^i Y ) e. _V )
5 fresin 
 |-  ( F : X --> ( 0 [,] +oo ) -> ( F |` Y ) : ( X i^i Y ) --> ( 0 [,] +oo ) )
6 2 5 syl 
 |-  ( ph -> ( F |` Y ) : ( X i^i Y ) --> ( 0 [,] +oo ) )
7 4 6 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( F |` Y ) ) e. RR* )
8 pnfge 
 |-  ( ( sum^ ` ( F |` Y ) ) e. RR* -> ( sum^ ` ( F |` Y ) ) <_ +oo )
9 7 8 syl 
 |-  ( ph -> ( sum^ ` ( F |` Y ) ) <_ +oo )
10 9 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` ( F |` Y ) ) <_ +oo )
11 id 
 |-  ( ( sum^ ` F ) = +oo -> ( sum^ ` F ) = +oo )
12 11 eqcomd 
 |-  ( ( sum^ ` F ) = +oo -> +oo = ( sum^ ` F ) )
13 12 adantl 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> +oo = ( sum^ ` F ) )
14 10 13 breqtrd 
 |-  ( ( ph /\ ( sum^ ` F ) = +oo ) -> ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) )
15 simpl 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ph )
16 simpr 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> -. ( sum^ ` F ) = +oo )
17 15 1 syl 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> X e. V )
18 15 2 syl 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> F : X --> ( 0 [,] +oo ) )
19 17 18 sge0repnf 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
20 16 19 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) e. RR )
21 elinel1 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) -> x e. ~P ( X i^i Y ) )
22 elpwi 
 |-  ( x e. ~P ( X i^i Y ) -> x C_ ( X i^i Y ) )
23 21 22 syl 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) -> x C_ ( X i^i Y ) )
24 inss2 
 |-  ( X i^i Y ) C_ Y
25 24 a1i 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) -> ( X i^i Y ) C_ Y )
26 23 25 sstrd 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) -> x C_ Y )
27 26 adantr 
 |-  ( ( x e. ( ~P ( X i^i Y ) i^i Fin ) /\ y e. x ) -> x C_ Y )
28 simpr 
 |-  ( ( x e. ( ~P ( X i^i Y ) i^i Fin ) /\ y e. x ) -> y e. x )
29 27 28 sseldd 
 |-  ( ( x e. ( ~P ( X i^i Y ) i^i Fin ) /\ y e. x ) -> y e. Y )
30 fvres 
 |-  ( y e. Y -> ( ( F |` Y ) ` y ) = ( F ` y ) )
31 29 30 syl 
 |-  ( ( x e. ( ~P ( X i^i Y ) i^i Fin ) /\ y e. x ) -> ( ( F |` Y ) ` y ) = ( F ` y ) )
32 31 ralrimiva 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) -> A. y e. x ( ( F |` Y ) ` y ) = ( F ` y ) )
33 32 sumeq2d 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) -> sum_ y e. x ( ( F |` Y ) ` y ) = sum_ y e. x ( F ` y ) )
34 33 mpteq2ia 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) = ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( F ` y ) )
35 inss1 
 |-  ( X i^i Y ) C_ X
36 35 sspwi 
 |-  ~P ( X i^i Y ) C_ ~P X
37 ssrin 
 |-  ( ~P ( X i^i Y ) C_ ~P X -> ( ~P ( X i^i Y ) i^i Fin ) C_ ( ~P X i^i Fin ) )
38 36 37 ax-mp 
 |-  ( ~P ( X i^i Y ) i^i Fin ) C_ ( ~P X i^i Fin )
39 mptss 
 |-  ( ( ~P ( X i^i Y ) i^i Fin ) C_ ( ~P X i^i Fin ) -> ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
40 38 39 ax-mp 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
41 34 40 eqsstri 
 |-  ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) C_ ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
42 rnss 
 |-  ( ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) C_ ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) -> ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) C_ ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
43 41 42 ax-mp 
 |-  ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) C_ ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
44 43 a1i 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) C_ ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
45 2 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> F : X --> ( 0 [,] +oo ) )
46 1 adantr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> X e. V )
47 simpr 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) e. RR )
48 46 45 47 sge0rern 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> -. +oo e. ran F )
49 45 48 fge0iccico 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> F : X --> ( 0 [,) +oo ) )
50 49 sge0rnre 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
51 ressxr 
 |-  RR C_ RR*
52 50 51 sstrdi 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
53 supxrss 
 |-  ( ( ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) C_ ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) /\ ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* ) -> sup ( ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) , RR* , < ) <_ sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
54 44 52 53 syl2anc 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> sup ( ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) , RR* , < ) <_ sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
55 46 3 syl 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( X i^i Y ) e. _V )
56 45 5 syl 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( F |` Y ) : ( X i^i Y ) --> ( 0 [,] +oo ) )
57 nelrnres 
 |-  ( -. +oo e. ran F -> -. +oo e. ran ( F |` Y ) )
58 48 57 syl 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> -. +oo e. ran ( F |` Y ) )
59 56 58 fge0iccico 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( F |` Y ) : ( X i^i Y ) --> ( 0 [,) +oo ) )
60 55 59 sge0reval 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` ( F |` Y ) ) = sup ( ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) , RR* , < ) )
61 46 49 sge0reval 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
62 60 61 breq12d 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) <-> sup ( ran ( x e. ( ~P ( X i^i Y ) i^i Fin ) |-> sum_ y e. x ( ( F |` Y ) ` y ) ) , RR* , < ) <_ sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) )
63 54 62 mpbird 
 |-  ( ( ph /\ ( sum^ ` F ) e. RR ) -> ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) )
64 15 20 63 syl2anc 
 |-  ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) )
65 14 64 pm2.61dan 
 |-  ( ph -> ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) )