Metamath Proof Explorer

Theorem sge0lessmpt

Description: A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lessmpt.a ⊢ φ → A ∈ V
sge0lessmpt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
sge0lessmpt.c ⊢ φ → C ⊆ A
Assertion sge0lessmpt ⊢ φ → sum^ ⁡ x ∈ C ⟼ B ≤ sum^ ⁡ x ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 sge0lessmpt.a ⊢ φ → A ∈ V
2 sge0lessmpt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
3 sge0lessmpt.c ⊢ φ → C ⊆ A
4 id ⊢ φ → φ
5 3 resmptd ⊢ φ → x ∈ A ⟼ B ↾ C = x ∈ C ⟼ B
6 5 eqcomd ⊢ φ → x ∈ C ⟼ B = x ∈ A ⟼ B ↾ C
7 4 6 syl ⊢ φ → x ∈ C ⟼ B = x ∈ A ⟼ B ↾ C
8 7 fveq2d ⊢ φ → sum^ ⁡ x ∈ C ⟼ B = sum^ ⁡ x ∈ A ⟼ B ↾ C
9 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
10 2 9 fmptd ⊢ φ → x ∈ A ⟼ B : A ⟶ 0 +∞
11 1 10 sge0less ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ↾ C ≤ sum^ ⁡ x ∈ A ⟼ B
12 8 11 eqbrtrd ⊢ φ → sum^ ⁡ x ∈ C ⟼ B ≤ sum^ ⁡ x ∈ A ⟼ B