Metamath Proof Explorer

Theorem sge0lempt

Description: If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lempt.xph 
|- F/ x ph
sge0lempt.a 
|- ( ph -> A e. V )
sge0lempt.b 
|- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
sge0lempt.c 
|- ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) )
sge0lempt.le 
|- ( ( ph /\ x e. A ) -> B <_ C )
Assertion sge0lempt 
|- ( ph -> ( sum^ ` ( x e. A |-> B ) ) <_ ( sum^ ` ( x e. A |-> C ) ) )

Proof

Step Hyp Ref Expression
1 sge0lempt.xph 
 |-  F/ x ph
2 sge0lempt.a 
 |-  ( ph -> A e. V )
3 sge0lempt.b 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )
4 sge0lempt.c 
 |-  ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) )
5 sge0lempt.le 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
6 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
7 1 3 6 fmptdf 
 |-  ( ph -> ( x e. A |-> B ) : A --> ( 0 [,] +oo ) )
8 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
9 1 4 8 fmptdf 
 |-  ( ph -> ( x e. A |-> C ) : A --> ( 0 [,] +oo ) )
10 nfv 
 |-  F/ x y e. A
11 1 10 nfan 
 |-  F/ x ( ph /\ y e. A )
12 nfcv 
 |-  F/_ x y
13 12 nfcsb1 
 |-  F/_ x [_ y / x ]_ B
14 nfcv 
 |-  F/_ x <_
15 12 nfcsb1 
 |-  F/_ x [_ y / x ]_ C
16 13 14 15 nfbr 
 |-  F/ x [_ y / x ]_ B <_ [_ y / x ]_ C
17 11 16 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B <_ [_ y / x ]_ C )
18 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
19 18 anbi2d 
 |-  ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) )
20 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
21 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
22 20 21 breq12d 
 |-  ( x = y -> ( B <_ C <-> [_ y / x ]_ B <_ [_ y / x ]_ C ) )
23 19 22 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B <_ C ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B <_ [_ y / x ]_ C ) ) )
24 17 23 5 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B <_ [_ y / x ]_ C )
25 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
26 13 nfel1 
 |-  F/ x [_ y / x ]_ B e. ( 0 [,] +oo )
27 11 26 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. ( 0 [,] +oo ) )
28 20 eleq1d 
 |-  ( x = y -> ( B e. ( 0 [,] +oo ) <-> [_ y / x ]_ B e. ( 0 [,] +oo ) ) )
29 19 28 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. ( 0 [,] +oo ) ) ) )
30 27 29 3 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. ( 0 [,] +oo ) )
31 12 13 20 6 fvmptf 
 |-  ( ( y e. A /\ [_ y / x ]_ B e. ( 0 [,] +oo ) ) -> ( ( x e. A |-> B ) ` y ) = [_ y / x ]_ B )
32 25 30 31 syl2anc 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> B ) ` y ) = [_ y / x ]_ B )
33 nfcv 
 |-  F/_ x ( 0 [,] +oo )
34 15 33 nfel 
 |-  F/ x [_ y / x ]_ C e. ( 0 [,] +oo )
35 11 34 nfim 
 |-  F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ C e. ( 0 [,] +oo ) )
36 21 eleq1d 
 |-  ( x = y -> ( C e. ( 0 [,] +oo ) <-> [_ y / x ]_ C e. ( 0 [,] +oo ) ) )
37 19 36 imbi12d 
 |-  ( x = y -> ( ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ C e. ( 0 [,] +oo ) ) ) )
38 35 37 4 chvarfv 
 |-  ( ( ph /\ y e. A ) -> [_ y / x ]_ C e. ( 0 [,] +oo ) )
39 12 15 21 8 fvmptf 
 |-  ( ( y e. A /\ [_ y / x ]_ C e. ( 0 [,] +oo ) ) -> ( ( x e. A |-> C ) ` y ) = [_ y / x ]_ C )
40 25 38 39 syl2anc 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> C ) ` y ) = [_ y / x ]_ C )
41 32 40 breq12d 
 |-  ( ( ph /\ y e. A ) -> ( ( ( x e. A |-> B ) ` y ) <_ ( ( x e. A |-> C ) ` y ) <-> [_ y / x ]_ B <_ [_ y / x ]_ C ) )
42 24 41 mpbird 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> B ) ` y ) <_ ( ( x e. A |-> C ) ` y ) )
43 2 7 9 42 sge0le 
 |-  ( ph -> ( sum^ ` ( x e. A |-> B ) ) <_ ( sum^ ` ( x e. A |-> C ) ) )