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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0resrn.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) )
	sge0resrn.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
	sge0resrn.r	⊢ ( 𝜑 → 𝑅 We 𝐴 )
Assertion	sge0resrn	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0resrn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sge0resrn.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) )
3		sge0resrn.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
4		sge0resrn.r	⊢ ( 𝜑 → 𝑅 We 𝐴 )
5	3	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
6	5 1 4	wessf1orn	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 )
7	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 ) → 𝐴 ∈ 𝑉 )
8	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 ) → 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) )
9	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 ) → 𝐺 : 𝐴 ⟶ 𝐵 )
10		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 ) → 𝑥 ∈ 𝒫 𝐴 )
11		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 ) → ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 )
12	7 8 9 10 11	sge0resrnlem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 ) → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) )
13	12	3exp	⊢ ( 𝜑 → ( 𝑥 ∈ 𝒫 𝐴 → ( ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) ) ) )
14	13	rexlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐺 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝐺 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) ) )
15	6 14	mpd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) )