Metamath Proof Explorer

Theorem sge0le

Description: If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0le.x 
|- ( ph -> X e. V )
sge0le.F 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0le.g 
|- ( ph -> G : X --> ( 0 [,] +oo ) )
sge0le.le 
|- ( ( ph /\ x e. X ) -> ( F ` x ) <_ ( G ` x ) )
Assertion sge0le 
|- ( ph -> ( sum^ ` F ) <_ ( sum^ ` G ) )

Proof

Step Hyp Ref Expression
1 sge0le.x 
 |-  ( ph -> X e. V )
2 sge0le.F 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0le.g 
 |-  ( ph -> G : X --> ( 0 [,] +oo ) )
4 sge0le.le 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) <_ ( G ` x ) )
5 1 2 sge0xrcl 
 |-  ( ph -> ( sum^ ` F ) e. RR* )
6 pnfge 
 |-  ( ( sum^ ` F ) e. RR* -> ( sum^ ` F ) <_ +oo )
7 5 6 syl 
 |-  ( ph -> ( sum^ ` F ) <_ +oo )
8 7 adantr 
 |-  ( ( ph /\ ( sum^ ` G ) = +oo ) -> ( sum^ ` F ) <_ +oo )
9 id 
 |-  ( ( sum^ ` G ) = +oo -> ( sum^ ` G ) = +oo )
10 9 eqcomd 
 |-  ( ( sum^ ` G ) = +oo -> +oo = ( sum^ ` G ) )
11 10 adantl 
 |-  ( ( ph /\ ( sum^ ` G ) = +oo ) -> +oo = ( sum^ ` G ) )
12 8 11 breqtrd 
 |-  ( ( ph /\ ( sum^ ` G ) = +oo ) -> ( sum^ ` F ) <_ ( sum^ ` G ) )
13 elinel2 
 |-  ( y e. ( ~P X i^i Fin ) -> y e. Fin )
14 13 adantl 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> y e. Fin )
15 2 adantr 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> F : X --> ( 0 [,] +oo ) )
16 1 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> X e. V )
17 3 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> G : X --> ( 0 [,] +oo ) )
18 simpr 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
19 2 ffnd 
 |-  ( ph -> F Fn X )
20 fvelrnb 
 |-  ( F Fn X -> ( +oo e. ran F <-> E. x e. X ( F ` x ) = +oo ) )
21 19 20 syl 
 |-  ( ph -> ( +oo e. ran F <-> E. x e. X ( F ` x ) = +oo ) )
22 21 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> ( +oo e. ran F <-> E. x e. X ( F ` x ) = +oo ) )
23 18 22 mpbid 
 |-  ( ( ph /\ +oo e. ran F ) -> E. x e. X ( F ` x ) = +oo )
24 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
25 3 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. ( 0 [,] +oo ) )
26 24 25 sselid 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. RR* )
27 26 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> ( G ` x ) e. RR* )
28 id 
 |-  ( ( F ` x ) = +oo -> ( F ` x ) = +oo )
29 28 eqcomd 
 |-  ( ( F ` x ) = +oo -> +oo = ( F ` x ) )
30 29 adantl 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> +oo = ( F ` x ) )
31 4 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> ( F ` x ) <_ ( G ` x ) )
32 30 31 eqbrtrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> +oo <_ ( G ` x ) )
33 27 32 xrgepnfd 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> ( G ` x ) = +oo )
34 33 eqcomd 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> +oo = ( G ` x ) )
35 3 ffnd 
 |-  ( ph -> G Fn X )
36 35 adantr 
 |-  ( ( ph /\ x e. X ) -> G Fn X )
37 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
38 fnfvelrn 
 |-  ( ( G Fn X /\ x e. X ) -> ( G ` x ) e. ran G )
39 36 37 38 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( G ` x ) e. ran G )
40 39 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> ( G ` x ) e. ran G )
41 34 40 eqeltrd 
 |-  ( ( ( ph /\ x e. X ) /\ ( F ` x ) = +oo ) -> +oo e. ran G )
42 41 ex 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) = +oo -> +oo e. ran G ) )
43 42 adantlr 
 |-  ( ( ( ph /\ +oo e. ran F ) /\ x e. X ) -> ( ( F ` x ) = +oo -> +oo e. ran G ) )
44 43 rexlimdva 
 |-  ( ( ph /\ +oo e. ran F ) -> ( E. x e. X ( F ` x ) = +oo -> +oo e. ran G ) )
45 23 44 mpd 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran G )
46 16 17 45 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` G ) = +oo )
47 46 adantlr 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ +oo e. ran F ) -> ( sum^ ` G ) = +oo )
48 simplr 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ +oo e. ran F ) -> -. ( sum^ ` G ) = +oo )
49 47 48 pm2.65da 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> -. +oo e. ran F )
50 15 49 fge0iccico 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> F : X --> ( 0 [,) +oo ) )
51 50 adantr 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,) +oo ) )
52 elpwinss 
 |-  ( y e. ( ~P X i^i Fin ) -> y C_ X )
53 52 adantl 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> y C_ X )
54 51 53 fssresd 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( F |` y ) : y --> ( 0 [,) +oo ) )
55 14 54 sge0fsum 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` y ) ) = sum_ x e. y ( ( F |` y ) ` x ) )
56 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
57 54 ffvelrnda 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( F |` y ) ` x ) e. ( 0 [,) +oo ) )
58 56 57 sselid 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( F |` y ) ` x ) e. RR )
59 14 58 fsumrecl 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( ( F |` y ) ` x ) e. RR )
60 55 59 eqeltrd 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` y ) ) e. RR )
61 3 adantr 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> G : X --> ( 0 [,] +oo ) )
62 1 adantr 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> X e. V )
63 simpr 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> -. ( sum^ ` G ) = +oo )
64 62 61 sge0repnf 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> ( ( sum^ ` G ) e. RR <-> -. ( sum^ ` G ) = +oo ) )
65 63 64 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> ( sum^ ` G ) e. RR )
66 62 61 65 sge0rern 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> -. +oo e. ran G )
67 61 66 fge0iccico 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> G : X --> ( 0 [,) +oo ) )
68 67 adantr 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> G : X --> ( 0 [,) +oo ) )
69 68 53 fssresd 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( G |` y ) : y --> ( 0 [,) +oo ) )
70 14 69 sge0fsum 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( G |` y ) ) = sum_ x e. y ( ( G |` y ) ` x ) )
71 69 ffvelrnda 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( G |` y ) ` x ) e. ( 0 [,) +oo ) )
72 56 71 sselid 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( G |` y ) ` x ) e. RR )
73 14 72 fsumrecl 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( ( G |` y ) ` x ) e. RR )
74 70 73 eqeltrd 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( G |` y ) ) e. RR )
75 65 adantr 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` G ) e. RR )
76 simplll 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ph )
77 53 sselda 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> x e. X )
78 76 77 4 syl2anc 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( F ` x ) <_ ( G ` x ) )
79 fvres 
 |-  ( x e. y -> ( ( F |` y ) ` x ) = ( F ` x ) )
80 79 adantl 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( F |` y ) ` x ) = ( F ` x ) )
81 fvres 
 |-  ( x e. y -> ( ( G |` y ) ` x ) = ( G ` x ) )
82 81 adantl 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( G |` y ) ` x ) = ( G ` x ) )
83 80 82 breq12d 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( ( F |` y ) ` x ) <_ ( ( G |` y ) ` x ) <-> ( F ` x ) <_ ( G ` x ) ) )
84 78 83 mpbird 
 |-  ( ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( ( F |` y ) ` x ) <_ ( ( G |` y ) ` x ) )
85 14 58 72 84 fsumle 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( ( F |` y ) ` x ) <_ sum_ x e. y ( ( G |` y ) ` x ) )
86 55 70 breq12d 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( ( sum^ ` ( F |` y ) ) <_ ( sum^ ` ( G |` y ) ) <-> sum_ x e. y ( ( F |` y ) ` x ) <_ sum_ x e. y ( ( G |` y ) ` x ) ) )
87 85 86 mpbird 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` y ) ) <_ ( sum^ ` ( G |` y ) ) )
88 1 adantr 
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> X e. V )
89 3 adantr 
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> G : X --> ( 0 [,] +oo ) )
90 88 89 sge0less 
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( G |` y ) ) <_ ( sum^ ` G ) )
91 90 adantlr 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( G |` y ) ) <_ ( sum^ ` G ) )
92 60 74 75 87 91 letrd 
 |-  ( ( ( ph /\ -. ( sum^ ` G ) = +oo ) /\ y e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` y ) ) <_ ( sum^ ` G ) )
93 92 ralrimiva 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> A. y e. ( ~P X i^i Fin ) ( sum^ ` ( F |` y ) ) <_ ( sum^ ` G ) )
94 62 61 sge0xrcl 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> ( sum^ ` G ) e. RR* )
95 62 15 94 sge0lefi 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> ( ( sum^ ` F ) <_ ( sum^ ` G ) <-> A. y e. ( ~P X i^i Fin ) ( sum^ ` ( F |` y ) ) <_ ( sum^ ` G ) ) )
96 93 95 mpbird 
 |-  ( ( ph /\ -. ( sum^ ` G ) = +oo ) -> ( sum^ ` F ) <_ ( sum^ ` G ) )
97 12 96 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) <_ ( sum^ ` G ) )