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 ⊢ φ → A ∈ V
sge0resrnlem.f ⊢ φ → F : B ⟶ 0 +∞
sge0resrnlem.g ⊢ φ → G : A ⟶ B
sge0resrnlem.x ⊢ φ → X ∈ 𝒫 A
sge0resrnlem.f1o ⊢ φ → G ↾ X : X ⟶ 1-1 onto ran ⁡ G
Assertion sge0resrnlem ⊢ φ → sum^ ⁡ F ↾ ran ⁡ G ≤ sum^ ⁡ F ∘ G

Proof

Step Hyp Ref Expression
1 sge0resrnlem.a ⊢ φ → A ∈ V
2 sge0resrnlem.f ⊢ φ → F : B ⟶ 0 +∞
3 sge0resrnlem.g ⊢ φ → G : A ⟶ B
4 sge0resrnlem.x ⊢ φ → X ∈ 𝒫 A
5 sge0resrnlem.f1o ⊢ φ → G ↾ X : X ⟶ 1-1 onto ran ⁡ G
6 nfv ⊢ Ⅎ y φ
7 nfv ⊢ Ⅎ x φ
8 fveq2 ⊢ y = G ⁡ x → F ⁡ y = F ⁡ G ⁡ x
9 fvres ⊢ x ∈ X → G ↾ X ⁡ x = G ⁡ x
10 9 adantl ⊢ φ ∧ x ∈ X → G ↾ X ⁡ x = G ⁡ x
11 2 adantr ⊢ φ ∧ y ∈ ran ⁡ G → F : B ⟶ 0 +∞
12 3 frnd ⊢ φ → ran ⁡ G ⊆ B
13 12 adantr ⊢ φ ∧ y ∈ ran ⁡ G → ran ⁡ G ⊆ B
14 simpr ⊢ φ ∧ y ∈ ran ⁡ G → y ∈ ran ⁡ G
15 13 14 sseldd ⊢ φ ∧ y ∈ ran ⁡ G → y ∈ B
16 11 15 ffvelcdmd ⊢ φ ∧ y ∈ ran ⁡ G → F ⁡ y ∈ 0 +∞
17 6 7 8 4 5 10 16 sge0f1o ⊢ φ → sum^ ⁡ y ∈ ran ⁡ G ⟼ F ⁡ y = sum^ ⁡ x ∈ X ⟼ F ⁡ G ⁡ x
18 2 12 feqresmpt ⊢ φ → F ↾ ran ⁡ G = y ∈ ran ⁡ G ⟼ F ⁡ y
19 18 fveq2d ⊢ φ → sum^ ⁡ F ↾ ran ⁡ G = sum^ ⁡ y ∈ ran ⁡ G ⟼ F ⁡ y
20 fcompt ⊢ F : B ⟶ 0 +∞ ∧ G : A ⟶ B → F ∘ G = x ∈ A ⟼ F ⁡ G ⁡ x
21 2 3 20 syl2anc ⊢ φ → F ∘ G = x ∈ A ⟼ F ⁡ G ⁡ x
22 21 reseq1d ⊢ φ → F ∘ G ↾ X = x ∈ A ⟼ F ⁡ G ⁡ x ↾ X
23 4 elpwid ⊢ φ → X ⊆ A
24 23 resmptd ⊢ φ → x ∈ A ⟼ F ⁡ G ⁡ x ↾ X = x ∈ X ⟼ F ⁡ G ⁡ x
25 22 24 eqtrd ⊢ φ → F ∘ G ↾ X = x ∈ X ⟼ F ⁡ G ⁡ x
26 25 fveq2d ⊢ φ → sum^ ⁡ F ∘ G ↾ X = sum^ ⁡ x ∈ X ⟼ F ⁡ G ⁡ x
27 17 19 26 3eqtr4d ⊢ φ → sum^ ⁡ F ↾ ran ⁡ G = sum^ ⁡ F ∘ G ↾ X
28 fco ⊢ F : B ⟶ 0 +∞ ∧ G : A ⟶ B → F ∘ G : A ⟶ 0 +∞
29 2 3 28 syl2anc ⊢ φ → F ∘ G : A ⟶ 0 +∞
30 1 29 sge0less ⊢ φ → sum^ ⁡ F ∘ G ↾ X ≤ sum^ ⁡ F ∘ G
31 27 30 eqbrtrd ⊢ φ → sum^ ⁡ F ↾ ran ⁡ G ≤ sum^ ⁡ F ∘ G