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
|- ( ph -> A e. V )
sge0lessmpt.b
|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
sge0lessmpt.c
|- ( ph -> C C_ A )
Assertion sge0lessmpt
|- ( ph -> ( sum^ ` ( x e. C |-> B ) ) <_ ( sum^ ` ( x e. A |-> B ) ) )

Proof

Step Hyp Ref Expression
1 sge0lessmpt.a
 |-  ( ph -> A e. V )
2 sge0lessmpt.b
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
3 sge0lessmpt.c
 |-  ( ph -> C C_ A )
4 id
 |-  ( ph -> ph )
5 3 resmptd
 |-  ( ph -> ( ( x e. A |-> B ) |` C ) = ( x e. C |-> B ) )
6 5 eqcomd
 |-  ( ph -> ( x e. C |-> B ) = ( ( x e. A |-> B ) |` C ) )
7 4 6 syl
 |-  ( ph -> ( x e. C |-> B ) = ( ( x e. A |-> B ) |` C ) )
8 7 fveq2d
 |-  ( ph -> ( sum^ ` ( x e. C |-> B ) ) = ( sum^ ` ( ( x e. A |-> B ) |` C ) ) )
9 eqid
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
10 2 9 fmptd
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
11 1 10 sge0less
 |-  ( ph -> ( sum^ ` ( ( x e. A |-> B ) |` C ) ) <_ ( sum^ ` ( x e. A |-> B ) ) )
12 8 11 eqbrtrd
 |-  ( ph -> ( sum^ ` ( x e. C |-> B ) ) <_ ( sum^ ` ( x e. A |-> B ) ) )