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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
sge0less.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
Assertion sge0less ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 sge0less.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2 sge0less.2 ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 inex1g ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∩ 𝑌 ) ∈ V )
4 1 3 syl ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ∈ V )
5 fresin ⊢ ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → ( 𝐹 ↾ 𝑌 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ( 0 [,] +∞ ) )
6 2 5 syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑌 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ( 0 [,] +∞ ) )
7 4 6 sge0xrcl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ* )
8 pnfge ⊢ ( ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ* → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ +∞ )
9 7 8 syl ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ +∞ )
10 9 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ +∞ )
11 id ⊢ ( ( Σ^ ‘ 𝐹 ) = +∞ → ( Σ^ ‘ 𝐹 ) = +∞ )
12 11 eqcomd ⊢ ( ( Σ^ ‘ 𝐹 ) = +∞ → +∞ = ( Σ^ ‘ 𝐹 ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → +∞ = ( Σ^ ‘ 𝐹 ) )
14 10 13 breqtrd ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) )
15 simpl ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → 𝜑 )
16 simpr ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ¬ ( Σ^ ‘ 𝐹 ) = +∞ )
17 15 1 syl ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → 𝑋 ∈ 𝑉 )
18 15 2 syl ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
19 17 18 sge0repnf ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( ( Σ^ ‘ 𝐹 ) ∈ ℝ ↔ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) )
20 16 19 mpbird ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
21 elinel1 ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) → 𝑥 ∈ 𝒫 ( 𝑋 ∩ 𝑌 ) )
22 elpwi ⊢ ( 𝑥 ∈ 𝒫 ( 𝑋 ∩ 𝑌 ) → 𝑥 ⊆ ( 𝑋 ∩ 𝑌 ) )
23 21 22 syl ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) → 𝑥 ⊆ ( 𝑋 ∩ 𝑌 ) )
24 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
25 24 a1i ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 )
26 23 25 sstrd ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) → 𝑥 ⊆ 𝑌 )
27 26 adantr ⊢ ( ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ⊆ 𝑌 )
28 simpr ⊢ ( ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
29 27 28 sseldd ⊢ ( ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑌 )
30 fvres ⊢ ( 𝑦 ∈ 𝑌 → ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
31 29 30 syl ⊢ ( ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
32 31 ralrimiva ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) → ∀ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
33 32 sumeq2d ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) → Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) = Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
34 33 mpteq2ia ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
35 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
36 35 sspwi ⊢ 𝒫 ( 𝑋 ∩ 𝑌 ) ⊆ 𝒫 𝑋
37 ssrin ⊢ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ⊆ 𝒫 𝑋 → ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ⊆ ( 𝒫 𝑋 ∩ Fin ) )
38 36 37 ax-mp ⊢ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ⊆ ( 𝒫 𝑋 ∩ Fin )
39 mptss ⊢ ( ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ⊆ ( 𝒫 𝑋 ∩ Fin ) → ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
40 38 39 ax-mp ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
41 34 40 eqsstri ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) ⊆ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
42 rnss ⊢ ( ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) ⊆ ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) → ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
43 41 42 ax-mp ⊢ ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) )
44 43 a1i ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) )
45 2 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
46 1 adantr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝑋 ∈ 𝑉 )
47 simpr ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) ∈ ℝ )
48 46 45 47 sge0rern ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ¬ +∞ ∈ ran 𝐹 )
49 45 48 fge0iccico ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
50 49 sge0rnre ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ )
51 ressxr ⊢ ℝ ⊆ ℝ*
52 50 51 sstrdi ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* )
53 supxrss ⊢ ( ( ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) ⊆ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ∧ ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) ⊆ ℝ* ) → sup ( ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
54 44 52 53 syl2anc ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → sup ( ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
55 46 3 syl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( 𝑋 ∩ 𝑌 ) ∈ V )
56 45 5 syl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( 𝐹 ↾ 𝑌 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ( 0 [,] +∞ ) )
57 nelrnres ⊢ ( ¬ +∞ ∈ ran 𝐹 → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝑌 ) )
58 48 57 syl ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ¬ +∞ ∈ ran ( 𝐹 ↾ 𝑌 ) )
59 56 58 fge0iccico ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( 𝐹 ↾ 𝑌 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ( 0 [,) +∞ ) )
60 55 59 sge0reval ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) , ℝ* , < ) )
61 46 49 sge0reval ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
62 60 61 breq12d ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) ↔ sup ( ran ( 𝑥 ∈ ( 𝒫 ( 𝑋 ∩ 𝑌 ) ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ( 𝐹 ↾ 𝑌 ) ‘ 𝑦 ) ) , ℝ* , < ) ≤ sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) )
63 54 62 mpbird ⊢ ( ( 𝜑 ∧ ( Σ^ ‘ 𝐹 ) ∈ ℝ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) )
64 15 20 63 syl2anc ⊢ ( ( 𝜑 ∧ ¬ ( Σ^ ‘ 𝐹 ) = +∞ ) → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) )
65 14 64 pm2.61dan ⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ≤ ( Σ^ ‘ 𝐹 ) )