Metamath Proof Explorer

Theorem itg2itg1

Description: The integral of a nonnegative simple function using S.2 is the same as its value under S.1 . (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itg2itg1 ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫2 ‘ 𝐹 ) = ( ∫1 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
2 xrge0f ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
3 1 2 sylan ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
4 itg2cl ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
5 3 4 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ* )
6 itg1cl ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
7 6 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
8 7 rexrd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐹 ) ∈ ℝ* )
9 itg1le ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ∧ 𝑔 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) )
10 9 3expia ⊢ ( ( 𝑔 ∈ dom ∫1 ∧ 𝐹 ∈ dom ∫1 ) → ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) ) )
11 10 ancoms ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1 ) → ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) ) )
12 11 ralrimiva ⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) ) )
13 12 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) ) )
14 itg2leub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫1 ‘ 𝐹 ) ∈ ℝ* ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐹 ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) ) ) )
15 3 8 14 syl2anc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ( ∫2 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐹 ) ↔ ∀ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 → ( ∫1 ‘ 𝑔 ) ≤ ( ∫1 ‘ 𝐹 ) ) ) )
16 13 15 mpbird ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫2 ‘ 𝐹 ) ≤ ( ∫1 ‘ 𝐹 ) )
17 simpl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 ∈ dom ∫1 )
18 reex ⊢ ℝ ∈ V
19 18 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ∈ V )
20 leid ⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ 𝑥 )
21 20 adantl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 𝑥 ≤ 𝑥 )
22 19 1 21 caofref ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∘r ≤ 𝐹 )
23 22 adantr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → 𝐹 ∘r ≤ 𝐹 )
24 itg2ub ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 ∈ dom ∫1 ∧ 𝐹 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐹 ) )
25 3 17 23 24 syl3anc ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐹 ) ≤ ( ∫2 ‘ 𝐹 ) )
26 5 8 16 25 xrletrid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ 𝐹 ) → ( ∫2 ‘ 𝐹 ) = ( ∫1 ‘ 𝐹 ) )