This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itg2val

Description: Value of the integral on nonnegative real functions. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Hypothesis itg2val.1 ⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
Assertion itg2val ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) = sup ( 𝐿 , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 itg2val.1 ⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2 xrltso ⊢ < Or ℝ*
3 2 supex ⊢ sup ( 𝐿 , ℝ* , < ) ∈ V
4 reex ⊢ ℝ ∈ V
5 ovex ⊢ ( 0 [,] +∞ ) ∈ V
6 breq2 ⊢ ( 𝑓 = 𝐹 → ( 𝑔 ∘r ≤ 𝑓 ↔ 𝑔 ∘r ≤ 𝐹 ) )
7 6 anbi1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ) )
8 7 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ) )
9 8 abbidv ⊢ ( 𝑓 = 𝐹 → { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } )
10 9 1 eqtr4di ⊢ ( 𝑓 = 𝐹 → { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } = 𝐿 )
11 10 supeq1d ⊢ ( 𝑓 = 𝐹 → sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) = sup ( 𝐿 , ℝ* , < ) )
12 df-itg2 ⊢ ∫2 = ( 𝑓 ∈ ( ( 0 [,] +∞ ) ↑m ℝ ) ↦ sup ( { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝑓 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } , ℝ* , < ) )
13 3 4 5 11 12 fvmptmap ⊢ ( 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) → ( ∫2 ‘ 𝐹 ) = sup ( 𝐿 , ℝ* , < ) )