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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
fsumlesge0.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
fsumlesge0.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
fsumlesge0.fi ⊢ ( 𝜑 → 𝑌 ∈ Fin )
Assertion fsumlesge0 ( 𝜑 → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ≤ ( Σ^ ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 fsumlesge0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 fsumlesge0.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
3 fsumlesge0.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4 fsumlesge0.fi ⊢ ( 𝜑 → 𝑌 ∈ Fin )
5 2 sge0rnre ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) ⊆ ℝ )
6 ressxr ⊢ ℝ ⊆ ℝ*
7 6 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
8 5 7 sstrd ⊢ ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) ⊆ ℝ* )
9 1 3 ssexd ⊢ ( 𝜑 → 𝑌 ∈ V )
10 elpwg ⊢ ( 𝑌 ∈ V → ( 𝑌 ∈ 𝒫 𝑋 ↔ 𝑌 ⊆ 𝑋 ) )
11 9 10 syl ⊢ ( 𝜑 → ( 𝑌 ∈ 𝒫 𝑋 ↔ 𝑌 ⊆ 𝑋 ) )
12 3 11 mpbird ⊢ ( 𝜑 → 𝑌 ∈ 𝒫 𝑋 )
13 12 4 elind ⊢ ( 𝜑 → 𝑌 ∈ ( 𝒫 𝑋 ∩ Fin ) )
14 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
15 14 cbvsumv ⊢ Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 )
16 15 a1i ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) )
17 sumeq1 ⊢ ( 𝑦 = 𝑌 → Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) = Σ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) )
18 17 rspceeqv ⊢ ( ( 𝑌 ∈ ( 𝒫 𝑋 ∩ Fin ) ∧ Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) )
19 13 16 18 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) )
20 sumex ⊢ Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ V
21 20 a1i ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ V )
22 eqid ⊢ ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) = ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) )
23 22 elrnmpt ⊢ ( Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ V → ( Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) )
24 21 23 syl ⊢ ( 𝜑 → ( Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) = Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) )
25 19 24 mpbird ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) )
26 supxrub ⊢ ( ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) ⊆ ℝ* ∧ Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ∈ ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) ) → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ≤ sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) , ℝ* , < ) )
27 8 25 26 syl2anc ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ≤ sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) , ℝ* , < ) )
28 1 2 sge0reval ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) , ℝ* , < ) )
29 28 eqcomd ⊢ ( 𝜑 → sup ( ran ( 𝑦 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑧 ∈ 𝑦 ( 𝐹 ‘ 𝑧 ) ) , ℝ* , < ) = ( Σ^ ‘ 𝐹 ) )
30 27 29 breqtrd ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑌 ( 𝐹 ‘ 𝑥 ) ≤ ( Σ^ ‘ 𝐹 ) )