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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0resrnlem.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) )
	sge0resrnlem.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
	sge0resrnlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝐴 )
	sge0resrnlem.f1o	⊢ ( 𝜑 → ( 𝐺 ↾ 𝑋 ) : 𝑋 –1-1-onto→ ran 𝐺 )
Assertion	sge0resrnlem	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0resrnlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sge0resrnlem.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) )
3		sge0resrnlem.g	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
4		sge0resrnlem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝒫 𝐴 )
5		sge0resrnlem.f1o	⊢ ( 𝜑 → ( 𝐺 ↾ 𝑋 ) : 𝑋 –1-1-onto→ ran 𝐺 )
6		nfv	⊢ Ⅎ 𝑦 𝜑
7		nfv	⊢ Ⅎ 𝑥 𝜑
8		fveq2	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) )
9		fvres	⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐺 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
11	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) )
12	3	frnd	⊢ ( 𝜑 → ran 𝐺 ⊆ 𝐵 )
13	12	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → ran 𝐺 ⊆ 𝐵 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → 𝑦 ∈ ran 𝐺 )
15	13 14	sseldd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → 𝑦 ∈ 𝐵 )
16	11 15	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 0 [,] +∞ ) )
17	6 7 8 4 5 10 16	sge0f1o	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑦 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑦 ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
18	2 12	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ ran 𝐺 ) = ( 𝑦 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑦 ) ) )
19	18	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) = ( Σ^ ‘ ( 𝑦 ∈ ran 𝐺 ↦ ( 𝐹 ‘ 𝑦 ) ) ) )
20		fcompt	⊢ ( ( 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
21	2 3 20	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
22	21	reseq1d	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ↾ 𝑋 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ↾ 𝑋 ) )
23	4	elpwid	⊢ ( 𝜑 → 𝑋 ⊆ 𝐴 )
24	23	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
25	22 24	eqtrd	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐺 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
26	25	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( ( 𝐹 ∘ 𝐺 ) ↾ 𝑋 ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
27	17 19 26	3eqtr4d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) = ( Σ^ ‘ ( ( 𝐹 ∘ 𝐺 ) ↾ 𝑋 ) ) )
28		fco	⊢ ( ( 𝐹 : 𝐵 ⟶ ( 0 [,] +∞ ) ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
29	2 3 28	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
30	1 29	sge0less	⊢ ( 𝜑 → ( Σ^ ‘ ( ( 𝐹 ∘ 𝐺 ) ↾ 𝑋 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) )
31	27 30	eqbrtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ ran 𝐺 ) ) ≤ ( Σ^ ‘ ( 𝐹 ∘ 𝐺 ) ) )