Metamath Proof Explorer

Theorem sge0resrnlem

Description: The sum of nonnegative extended reals restricted to the range of a function is less than or equal to the sum of the composition of the two functions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0resrnlem.a 
|- ( ph -> A e. V )
sge0resrnlem.f 
|- ( ph -> F : B --> ( 0 [,] +oo ) )
sge0resrnlem.g 
|- ( ph -> G : A --> B )
sge0resrnlem.x 
|- ( ph -> X e. ~P A )
sge0resrnlem.f1o 
|- ( ph -> ( G |` X ) : X -1-1-onto-> ran G )
Assertion sge0resrnlem 
|- ( ph -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) )

Proof

Step Hyp Ref Expression
1 sge0resrnlem.a 
 |-  ( ph -> A e. V )
2 sge0resrnlem.f 
 |-  ( ph -> F : B --> ( 0 [,] +oo ) )
3 sge0resrnlem.g 
 |-  ( ph -> G : A --> B )
4 sge0resrnlem.x 
 |-  ( ph -> X e. ~P A )
5 sge0resrnlem.f1o 
 |-  ( ph -> ( G |` X ) : X -1-1-onto-> ran G )
6 nfv 
 |-  F/ y ph
7 nfv 
 |-  F/ x ph
8 fveq2 
 |-  ( y = ( G ` x ) -> ( F ` y ) = ( F ` ( G ` x ) ) )
9 fvres 
 |-  ( x e. X -> ( ( G |` X ) ` x ) = ( G ` x ) )
10 9 adantl 
 |-  ( ( ph /\ x e. X ) -> ( ( G |` X ) ` x ) = ( G ` x ) )
11 2 adantr 
 |-  ( ( ph /\ y e. ran G ) -> F : B --> ( 0 [,] +oo ) )
12 3 frnd 
 |-  ( ph -> ran G C_ B )
13 12 adantr 
 |-  ( ( ph /\ y e. ran G ) -> ran G C_ B )
14 simpr 
 |-  ( ( ph /\ y e. ran G ) -> y e. ran G )
15 13 14 sseldd 
 |-  ( ( ph /\ y e. ran G ) -> y e. B )
16 11 15 ffvelcdmd 
 |-  ( ( ph /\ y e. ran G ) -> ( F ` y ) e. ( 0 [,] +oo ) )
17 6 7 8 4 5 10 16 sge0f1o 
 |-  ( ph -> ( sum^ ` ( y e. ran G |-> ( F ` y ) ) ) = ( sum^ ` ( x e. X |-> ( F ` ( G ` x ) ) ) ) )
18 2 12 feqresmpt 
 |-  ( ph -> ( F |` ran G ) = ( y e. ran G |-> ( F ` y ) ) )
19 18 fveq2d 
 |-  ( ph -> ( sum^ ` ( F |` ran G ) ) = ( sum^ ` ( y e. ran G |-> ( F ` y ) ) ) )
20 fcompt 
 |-  ( ( F : B --> ( 0 [,] +oo ) /\ G : A --> B ) -> ( F o. G ) = ( x e. A |-> ( F ` ( G ` x ) ) ) )
21 2 3 20 syl2anc 
 |-  ( ph -> ( F o. G ) = ( x e. A |-> ( F ` ( G ` x ) ) ) )
22 21 reseq1d 
 |-  ( ph -> ( ( F o. G ) |` X ) = ( ( x e. A |-> ( F ` ( G ` x ) ) ) |` X ) )
23 4 elpwid 
 |-  ( ph -> X C_ A )
24 23 resmptd 
 |-  ( ph -> ( ( x e. A |-> ( F ` ( G ` x ) ) ) |` X ) = ( x e. X |-> ( F ` ( G ` x ) ) ) )
25 22 24 eqtrd 
 |-  ( ph -> ( ( F o. G ) |` X ) = ( x e. X |-> ( F ` ( G ` x ) ) ) )
26 25 fveq2d 
 |-  ( ph -> ( sum^ ` ( ( F o. G ) |` X ) ) = ( sum^ ` ( x e. X |-> ( F ` ( G ` x ) ) ) ) )
27 17 19 26 3eqtr4d 
 |-  ( ph -> ( sum^ ` ( F |` ran G ) ) = ( sum^ ` ( ( F o. G ) |` X ) ) )
28 fco 
 |-  ( ( F : B --> ( 0 [,] +oo ) /\ G : A --> B ) -> ( F o. G ) : A --> ( 0 [,] +oo ) )
29 2 3 28 syl2anc 
 |-  ( ph -> ( F o. G ) : A --> ( 0 [,] +oo ) )
30 1 29 sge0less 
 |-  ( ph -> ( sum^ ` ( ( F o. G ) |` X ) ) <_ ( sum^ ` ( F o. G ) ) )
31 27 30 eqbrtrd 
 |-  ( ph -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) )