This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrge0gsumle

Description: A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypotheses xrge0gsumle.g 
|- G = ( RR*s |`s ( 0 [,] +oo ) )
xrge0gsumle.a 
|- ( ph -> A e. V )
xrge0gsumle.f 
|- ( ph -> F : A --> ( 0 [,] +oo ) )
xrge0gsumle.b 
|- ( ph -> B e. ( ~P A i^i Fin ) )
xrge0gsumle.c 
|- ( ph -> C C_ B )
Assertion xrge0gsumle 
|- ( ph -> ( G gsum ( F |` C ) ) <_ ( G gsum ( F |` B ) ) )

Proof

Step Hyp Ref Expression
1 xrge0gsumle.g 
 |-  G = ( RR*s |`s ( 0 [,] +oo ) )
2 xrge0gsumle.a 
 |-  ( ph -> A e. V )
3 xrge0gsumle.f 
 |-  ( ph -> F : A --> ( 0 [,] +oo ) )
4 xrge0gsumle.b 
 |-  ( ph -> B e. ( ~P A i^i Fin ) )
5 xrge0gsumle.c 
 |-  ( ph -> C C_ B )
6 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
7 xrsbas 
 |-  RR* = ( Base ` RR*s )
8 1 7 ressbas2 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( 0 [,] +oo ) = ( Base ` G ) )
9 6 8 ax-mp 
 |-  ( 0 [,] +oo ) = ( Base ` G )
10 eqid 
 |-  ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
11 10 xrge0subm 
 |-  ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) )
12 xrex 
 |-  RR* e. _V
13 12 difexi 
 |-  ( RR* \ { -oo } ) e. _V
14 simpl 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> x e. RR* )
15 ge0nemnf 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> x =/= -oo )
16 14 15 jca 
 |-  ( ( x e. RR* /\ 0 <_ x ) -> ( x e. RR* /\ x =/= -oo ) )
17 elxrge0 
 |-  ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
18 eldifsn 
 |-  ( x e. ( RR* \ { -oo } ) <-> ( x e. RR* /\ x =/= -oo ) )
19 16 17 18 3imtr4i 
 |-  ( x e. ( 0 [,] +oo ) -> x e. ( RR* \ { -oo } ) )
20 19 ssriv 
 |-  ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
21 ressabs 
 |-  ( ( ( RR* \ { -oo } ) e. _V /\ ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) ) -> ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) ) )
22 13 20 21 mp2an 
 |-  ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
23 1 22 eqtr4i 
 |-  G = ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) )
24 10 xrs10 
 |-  0 = ( 0g ` ( RR*s |`s ( RR* \ { -oo } ) ) )
25 23 24 subm0 
 |-  ( ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) ) -> 0 = ( 0g ` G ) )
26 11 25 ax-mp 
 |-  0 = ( 0g ` G )
27 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
28 1 27 eqeltri 
 |-  G e. CMnd
29 28 a1i 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> G e. CMnd )
30 elfpw 
 |-  ( s e. ( ~P A i^i Fin ) <-> ( s C_ A /\ s e. Fin ) )
31 30 simprbi 
 |-  ( s e. ( ~P A i^i Fin ) -> s e. Fin )
32 31 adantl 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> s e. Fin )
33 30 simplbi 
 |-  ( s e. ( ~P A i^i Fin ) -> s C_ A )
34 fssres 
 |-  ( ( F : A --> ( 0 [,] +oo ) /\ s C_ A ) -> ( F |` s ) : s --> ( 0 [,] +oo ) )
35 3 33 34 syl2an 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( F |` s ) : s --> ( 0 [,] +oo ) )
36 c0ex 
 |-  0 e. _V
37 36 a1i 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> 0 e. _V )
38 35 32 37 fdmfifsupp 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( F |` s ) finSupp 0 )
39 9 26 29 32 35 38 gsumcl 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` s ) ) e. ( 0 [,] +oo ) )
40 6 39 sselid 
 |-  ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` s ) ) e. RR* )
41 40 fmpttd 
 |-  ( ph -> ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) : ( ~P A i^i Fin ) --> RR* )
42 41 frnd 
 |-  ( ph -> ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* )
43 0ss 
 |-  (/) C_ A
44 0fi 
 |-  (/) e. Fin
45 elfpw 
 |-  ( (/) e. ( ~P A i^i Fin ) <-> ( (/) C_ A /\ (/) e. Fin ) )
46 43 44 45 mpbir2an 
 |-  (/) e. ( ~P A i^i Fin )
47 0cn 
 |-  0 e. CC
48 eqid 
 |-  ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) = ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) )
49 reseq2 
 |-  ( s = (/) -> ( F |` s ) = ( F |` (/) ) )
50 res0 
 |-  ( F |` (/) ) = (/)
51 49 50 eqtrdi 
 |-  ( s = (/) -> ( F |` s ) = (/) )
52 51 oveq2d 
 |-  ( s = (/) -> ( G gsum ( F |` s ) ) = ( G gsum (/) ) )
53 26 gsum0 
 |-  ( G gsum (/) ) = 0
54 52 53 eqtrdi 
 |-  ( s = (/) -> ( G gsum ( F |` s ) ) = 0 )
55 48 54 elrnmpt1s 
 |-  ( ( (/) e. ( ~P A i^i Fin ) /\ 0 e. CC ) -> 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
56 46 47 55 mp2an 
 |-  0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) )
57 56 a1i 
 |-  ( ph -> 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
58 42 57 sseldd 
 |-  ( ph -> 0 e. RR* )
59 28 a1i 
 |-  ( ph -> G e. CMnd )
60 4 elin2d 
 |-  ( ph -> B e. Fin )
61 diffi 
 |-  ( B e. Fin -> ( B \ C ) e. Fin )
62 60 61 syl 
 |-  ( ph -> ( B \ C ) e. Fin )
63 elfpw 
 |-  ( B e. ( ~P A i^i Fin ) <-> ( B C_ A /\ B e. Fin ) )
64 63 simplbi 
 |-  ( B e. ( ~P A i^i Fin ) -> B C_ A )
65 4 64 syl 
 |-  ( ph -> B C_ A )
66 65 ssdifssd 
 |-  ( ph -> ( B \ C ) C_ A )
67 3 66 fssresd 
 |-  ( ph -> ( F |` ( B \ C ) ) : ( B \ C ) --> ( 0 [,] +oo ) )
68 36 a1i 
 |-  ( ph -> 0 e. _V )
69 67 62 68 fdmfifsupp 
 |-  ( ph -> ( F |` ( B \ C ) ) finSupp 0 )
70 9 26 59 62 67 69 gsumcl 
 |-  ( ph -> ( G gsum ( F |` ( B \ C ) ) ) e. ( 0 [,] +oo ) )
71 6 70 sselid 
 |-  ( ph -> ( G gsum ( F |` ( B \ C ) ) ) e. RR* )
72 60 5 ssfid 
 |-  ( ph -> C e. Fin )
73 5 65 sstrd 
 |-  ( ph -> C C_ A )
74 3 73 fssresd 
 |-  ( ph -> ( F |` C ) : C --> ( 0 [,] +oo ) )
75 74 72 68 fdmfifsupp 
 |-  ( ph -> ( F |` C ) finSupp 0 )
76 9 26 59 72 74 75 gsumcl 
 |-  ( ph -> ( G gsum ( F |` C ) ) e. ( 0 [,] +oo ) )
77 6 76 sselid 
 |-  ( ph -> ( G gsum ( F |` C ) ) e. RR* )
78 elxrge0 
 |-  ( ( G gsum ( F |` ( B \ C ) ) ) e. ( 0 [,] +oo ) <-> ( ( G gsum ( F |` ( B \ C ) ) ) e. RR* /\ 0 <_ ( G gsum ( F |` ( B \ C ) ) ) ) )
79 78 simprbi 
 |-  ( ( G gsum ( F |` ( B \ C ) ) ) e. ( 0 [,] +oo ) -> 0 <_ ( G gsum ( F |` ( B \ C ) ) ) )
80 70 79 syl 
 |-  ( ph -> 0 <_ ( G gsum ( F |` ( B \ C ) ) ) )
81 xleadd2a 
 |-  ( ( ( 0 e. RR* /\ ( G gsum ( F |` ( B \ C ) ) ) e. RR* /\ ( G gsum ( F |` C ) ) e. RR* ) /\ 0 <_ ( G gsum ( F |` ( B \ C ) ) ) ) -> ( ( G gsum ( F |` C ) ) +e 0 ) <_ ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) )
82 58 71 77 80 81 syl31anc 
 |-  ( ph -> ( ( G gsum ( F |` C ) ) +e 0 ) <_ ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) )
83 77 xaddridd 
 |-  ( ph -> ( ( G gsum ( F |` C ) ) +e 0 ) = ( G gsum ( F |` C ) ) )
84 ovex 
 |-  ( 0 [,] +oo ) e. _V
85 xrsadd 
 |-  +e = ( +g ` RR*s )
86 1 85 ressplusg 
 |-  ( ( 0 [,] +oo ) e. _V -> +e = ( +g ` G ) )
87 84 86 ax-mp 
 |-  +e = ( +g ` G )
88 3 65 fssresd 
 |-  ( ph -> ( F |` B ) : B --> ( 0 [,] +oo ) )
89 88 60 68 fdmfifsupp 
 |-  ( ph -> ( F |` B ) finSupp 0 )
90 disjdif 
 |-  ( C i^i ( B \ C ) ) = (/)
91 90 a1i 
 |-  ( ph -> ( C i^i ( B \ C ) ) = (/) )
92 undif2 
 |-  ( C u. ( B \ C ) ) = ( C u. B )
93 ssequn1 
 |-  ( C C_ B <-> ( C u. B ) = B )
94 5 93 sylib 
 |-  ( ph -> ( C u. B ) = B )
95 92 94 eqtr2id 
 |-  ( ph -> B = ( C u. ( B \ C ) ) )
96 9 26 87 59 4 88 89 91 95 gsumsplit 
 |-  ( ph -> ( G gsum ( F |` B ) ) = ( ( G gsum ( ( F |` B ) |` C ) ) +e ( G gsum ( ( F |` B ) |` ( B \ C ) ) ) ) )
97 5 resabs1d 
 |-  ( ph -> ( ( F |` B ) |` C ) = ( F |` C ) )
98 97 oveq2d 
 |-  ( ph -> ( G gsum ( ( F |` B ) |` C ) ) = ( G gsum ( F |` C ) ) )
99 difss 
 |-  ( B \ C ) C_ B
100 resabs1 
 |-  ( ( B \ C ) C_ B -> ( ( F |` B ) |` ( B \ C ) ) = ( F |` ( B \ C ) ) )
101 99 100 mp1i 
 |-  ( ph -> ( ( F |` B ) |` ( B \ C ) ) = ( F |` ( B \ C ) ) )
102 101 oveq2d 
 |-  ( ph -> ( G gsum ( ( F |` B ) |` ( B \ C ) ) ) = ( G gsum ( F |` ( B \ C ) ) ) )
103 98 102 oveq12d 
 |-  ( ph -> ( ( G gsum ( ( F |` B ) |` C ) ) +e ( G gsum ( ( F |` B ) |` ( B \ C ) ) ) ) = ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) )
104 96 103 eqtr2d 
 |-  ( ph -> ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) = ( G gsum ( F |` B ) ) )
105 82 83 104 3brtr3d 
 |-  ( ph -> ( G gsum ( F |` C ) ) <_ ( G gsum ( F |` B ) ) )