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	$⊢ φ \to A \in V$
	sge0resrn.f	$⊢ φ \to F : B ⟶ [0, +∞]$
	sge0resrn.g	$⊢ φ \to G : A ⟶ B$
	sge0resrn.r	$⊢ φ \to R We A$
Assertion	sge0resrn	$⊢ φ \to sum^({F ↾}_{ran G}) \leq sum^(F \circ G)$

Proof

Step	Hyp	Ref	Expression
1		sge0resrn.a	$⊢ φ \to A \in V$
2		sge0resrn.f	$⊢ φ \to F : B ⟶ [0, +∞]$
3		sge0resrn.g	$⊢ φ \to G : A ⟶ B$
4		sge0resrn.r	$⊢ φ \to R We A$
5	3	ffnd	$⊢ φ \to G Fn A$
6	5 1 4	wessf1orn	$⊢ φ \to \exists x \in 𝒫 A ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G$
7	1	3ad2ant1	$⊢ (φ \land x \in 𝒫 A \land ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G) \to A \in V$
8	2	3ad2ant1	$⊢ (φ \land x \in 𝒫 A \land ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G) \to F : B ⟶ [0, +∞]$
9	3	3ad2ant1	$⊢ (φ \land x \in 𝒫 A \land ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G) \to G : A ⟶ B$
10		simp2	$⊢ (φ \land x \in 𝒫 A \land ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G) \to x \in 𝒫 A$
11		simp3	$⊢ (φ \land x \in 𝒫 A \land ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G) \to ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G$
12	7 8 9 10 11	sge0resrnlem	$⊢ (φ \land x \in 𝒫 A \land ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G) \to sum^({F ↾}_{ran G}) \leq sum^(F \circ G)$
13	12	3exp	$⊢ φ \to (x \in 𝒫 A \to (({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G \to sum^({F ↾}_{ran G}) \leq sum^(F \circ G)))$
14	13	rexlimdv	$⊢ φ \to (\exists x \in 𝒫 A ({G ↾}_{x}) : x \underset{1-1 onto}{⟶} ran G \to sum^({F ↾}_{ran G}) \leq sum^(F \circ G))$
15	6 14	mpd	$⊢ φ \to sum^({F ↾}_{ran G}) \leq sum^(F \circ G)$

Metamath Proof Explorer

Theorem sge0resrn

Proof