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

Metamath Proof Explorer

Theorem cnbdibl

Description: A continuous bounded function is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cnbdibl.a ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
cnbdibl.va ⊢ ( 𝜑 → ( vol ‘ 𝐴 ) ∈ ℝ )
cnbdibl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
cnbdibl.bd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
Assertion cnbdibl ( 𝜑 → 𝐹 ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 cnbdibl.a ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
2 cnbdibl.va ⊢ ( 𝜑 → ( vol ‘ 𝐴 ) ∈ ℝ )
3 cnbdibl.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
4 cnbdibl.bd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 )
5 cnmbf ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( 𝐴 –cn→ ℂ ) ) → 𝐹 ∈ MblFn )
6 1 3 5 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
7 cncff ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
8 fdm ⊢ ( 𝐹 : 𝐴 ⟶ ℂ → dom 𝐹 = 𝐴 )
9 3 7 8 3syl ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
10 9 fveq2d ⊢ ( 𝜑 → ( vol ‘ dom 𝐹 ) = ( vol ‘ 𝐴 ) )
11 10 2 eqeltrd ⊢ ( 𝜑 → ( vol ‘ dom 𝐹 ) ∈ ℝ )
12 bddibl ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )
13 6 11 4 12 syl3anc ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )