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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0lessmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0lessmpt.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion	sge0lessmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0lessmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sge0lessmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
3		sge0lessmpt.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4		id	⊢ ( 𝜑 → 𝜑 )
5	3	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) )
6	5	eqcomd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) )
7	4 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) )
8	7	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) = ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) ) )
9		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
10	2 9	fmptd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
11	1 10	sge0less	⊢ ( 𝜑 → ( Σ^ ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↾ 𝐶 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
12	8 11	eqbrtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) ) ≤ ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )