Theorem sge0resrn

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 (well-order hypothesis allows to avoid using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0resrn.a	|- ( ph -> A e. V )
	sge0resrn.f	|- ( ph -> F : B --> ( 0 [,] +oo ) )
	sge0resrn.g	|- ( ph -> G : A --> B )
	sge0resrn.r	|- ( ph -> R We A )
Assertion	sge0resrn	|- ( ph -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0resrn.a	|- ( ph -> A e. V )
2		sge0resrn.f	|- ( ph -> F : B --> ( 0 [,] +oo ) )
3		sge0resrn.g	|- ( ph -> G : A --> B )
4		sge0resrn.r	|- ( ph -> R We A )
5	3	ffnd	|- ( ph -> G Fn A )
6	5 1 4	wessf1orn	|- ( ph -> E. x e. ~P A ( G |` x ) : x -1-1-onto-> ran G )
7	1	3ad2ant1	|- ( ( ph /\ x e. ~P A /\ ( G |` x ) : x -1-1-onto-> ran G ) -> A e. V )
8	2	3ad2ant1	|- ( ( ph /\ x e. ~P A /\ ( G |` x ) : x -1-1-onto-> ran G ) -> F : B --> ( 0 [,] +oo ) )
9	3	3ad2ant1	|- ( ( ph /\ x e. ~P A /\ ( G |` x ) : x -1-1-onto-> ran G ) -> G : A --> B )
10		simp2	|- ( ( ph /\ x e. ~P A /\ ( G |` x ) : x -1-1-onto-> ran G ) -> x e. ~P A )
11		simp3	|- ( ( ph /\ x e. ~P A /\ ( G |` x ) : x -1-1-onto-> ran G ) -> ( G |` x ) : x -1-1-onto-> ran G )
12	7 8 9 10 11	sge0resrnlem	|- ( ( ph /\ x e. ~P A /\ ( G |` x ) : x -1-1-onto-> ran G ) -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) )
13	12	3exp	|- ( ph -> ( x e. ~P A -> ( ( G |` x ) : x -1-1-onto-> ran G -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) ) ) )
14	13	rexlimdv	|- ( ph -> ( E. x e. ~P A ( G |` x ) : x -1-1-onto-> ran G -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) ) )
15	6 14	mpd	|- ( ph -> ( sum^ ` ( F |` ran G ) ) <_ ( sum^ ` ( F o. G ) ) )