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 ⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
xrge0gsumle.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
xrge0gsumle.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
xrge0gsumle.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) )
xrge0gsumle.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
Assertion xrge0gsumle ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ≤ ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 xrge0gsumle.g ⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2 xrge0gsumle.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 xrge0gsumle.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
4 xrge0gsumle.b ⊢ ( 𝜑 → 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) )
5 xrge0gsumle.c ⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
6 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
7 xrsbas ⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
8 1 7 ressbas2 ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( 0 [,] +∞ ) = ( Base ‘ 𝐺 ) )
9 6 8 ax-mp ⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝐺 )
10 eqid ⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
11 10 xrge0subm ⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
12 xrex ⊢ ℝ* ∈ V
13 12 difexi ⊢ ( ℝ* ∖ { -∞ } ) ∈ V
14 simpl ⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
15 ge0nemnf ⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → 𝑥 ≠ -∞ )
16 14 15 jca ⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
17 elxrge0 ⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) )
18 eldifsn ⊢ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
19 16 17 18 3imtr4i ⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ( ℝ* ∖ { -∞ } ) )
20 19 ssriv ⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
21 ressabs ⊢ ( ( ( ℝ* ∖ { -∞ } ) ∈ V ∧ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ) → ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
22 13 20 21 mp2an ⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
23 1 22 eqtr4i ⊢ 𝐺 = ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) )
24 10 xrs10 ⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
25 23 24 subm0 ⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) → 0 = ( 0g ‘ 𝐺 ) )
26 11 25 ax-mp ⊢ 0 = ( 0g ‘ 𝐺 )
27 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
28 1 27 eqeltri ⊢ 𝐺 ∈ CMnd
29 28 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
30 elfpw ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin ) )
31 30 simprbi ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑠 ∈ Fin )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑠 ∈ Fin )
33 30 simplbi ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑠 ⊆ 𝐴 )
34 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ∧ 𝑠 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑠 ) : 𝑠 ⟶ ( 0 [,] +∞ ) )
35 3 33 34 syl2an ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑠 ) : 𝑠 ⟶ ( 0 [,] +∞ ) )
36 c0ex ⊢ 0 ∈ V
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ∈ V )
38 35 32 37 fdmfifsupp ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑠 ) finSupp 0 )
39 9 26 29 32 35 38 gsumcl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ∈ ( 0 [,] +∞ ) )
40 6 39 sseldi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ∈ ℝ* )
41 40 fmpttd ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ ℝ* )
42 41 frnd ⊢ ( 𝜑 → ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) ⊆ ℝ* )
43 0ss ⊢ ∅ ⊆ 𝐴
44 0fin ⊢ ∅ ∈ Fin
45 elfpw ⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ∅ ⊆ 𝐴 ∧ ∅ ∈ Fin ) )
46 43 44 45 mpbir2an ⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
47 0cn ⊢ 0 ∈ ℂ
48 eqid ⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) )
49 reseq2 ⊢ ( 𝑠 = ∅ → ( 𝐹 ↾ 𝑠 ) = ( 𝐹 ↾ ∅ ) )
50 res0 ⊢ ( 𝐹 ↾ ∅ ) = ∅
51 49 50 eqtrdi ⊢ ( 𝑠 = ∅ → ( 𝐹 ↾ 𝑠 ) = ∅ )
52 51 oveq2d ⊢ ( 𝑠 = ∅ → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) = ( 𝐺 Σg ∅ ) )
53 26 gsum0 ⊢ ( 𝐺 Σg ∅ ) = 0
54 52 53 eqtrdi ⊢ ( 𝑠 = ∅ → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) = 0 )
55 48 54 elrnmpt1s ⊢ ( ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 0 ∈ ℂ ) → 0 ∈ ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) )
56 46 47 55 mp2an ⊢ 0 ∈ ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) )
57 56 a1i ⊢ ( 𝜑 → 0 ∈ ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) )
58 42 57 sseldd ⊢ ( 𝜑 → 0 ∈ ℝ* )
59 28 a1i ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
60 4 elin2d ⊢ ( 𝜑 → 𝐵 ∈ Fin )
61 diffi ⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∖ 𝐶 ) ∈ Fin )
62 60 61 syl ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐶 ) ∈ Fin )
63 elfpw ⊢ ( 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin ) )
64 63 simplbi ⊢ ( 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝐵 ⊆ 𝐴 )
65 4 64 syl ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
66 65 ssdifssd ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐶 ) ⊆ 𝐴 )
67 3 66 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) : ( 𝐵 ∖ 𝐶 ) ⟶ ( 0 [,] +∞ ) )
68 36 a1i ⊢ ( 𝜑 → 0 ∈ V )
69 67 62 68 fdmfifsupp ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) finSupp 0 )
70 9 26 59 62 67 69 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) )
71 6 70 sseldi ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ℝ* )
72 60 5 ssfid ⊢ ( 𝜑 → 𝐶 ∈ Fin )
73 5 65 sstrd ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
74 3 73 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ( 0 [,] +∞ ) )
75 74 72 68 fdmfifsupp ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) finSupp 0 )
76 9 26 59 72 74 75 gsumcl ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
77 6 76 sseldi ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ∈ ℝ* )
78 elxrge0 ⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ℝ* ∧ 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
79 78 simprbi ⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) )
80 70 79 syl ⊢ ( 𝜑 → 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) )
81 xleadd2a ⊢ ( ( ( 0 ∈ ℝ* ∧ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ℝ* ∧ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ∈ ℝ* ) ∧ 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 0 ) ≤ ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
82 58 71 77 80 81 syl31anc ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 0 ) ≤ ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
83 77 xaddid1d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 0 ) = ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) )
84 ovex ⊢ ( 0 [,] +∞ ) ∈ V
85 xrsadd ⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
86 1 85 ressplusg ⊢ ( ( 0 [,] +∞ ) ∈ V → +𝑒 = ( +g ‘ 𝐺 ) )
87 84 86 ax-mp ⊢ +𝑒 = ( +g ‘ 𝐺 )
88 3 65 fssresd ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
89 88 60 68 fdmfifsupp ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) finSupp 0 )
90 disjdif ⊢ ( 𝐶 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅
91 90 a1i ⊢ ( 𝜑 → ( 𝐶 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )
92 undif2 ⊢ ( 𝐶 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐶 ∪ 𝐵 )
93 ssequn1 ⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐶 ∪ 𝐵 ) = 𝐵 )
94 5 93 sylib ⊢ ( 𝜑 → ( 𝐶 ∪ 𝐵 ) = 𝐵 )
95 92 94 syl5req ⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∪ ( 𝐵 ∖ 𝐶 ) ) )
96 9 26 87 59 4 88 89 91 95 gsumsplit ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) = ( ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) ) +𝑒 ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
97 5 resabs1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) = ( 𝐹 ↾ 𝐶 ) )
98 97 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) )
99 difss ⊢ ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵
100 resabs1 ⊢ ( ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) )
101 99 100 mp1i ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) )
102 101 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) )
103 98 102 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) ) +𝑒 ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
104 96 103 eqtr2d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +𝑒 ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) )
105 82 83 104 3brtr3d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ≤ ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) )