Metamath Proof Explorer

Theorem cnbdibl

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

Ref Expression
Hypotheses cnbdibl.a ${⊢}{\phi }\to {A}\in \mathrm{dom}vol$
cnbdibl.va ${⊢}{\phi }\to vol\left({A}\right)\in ℝ$
cnbdibl.f ${⊢}{\phi }\to {F}:{A}\underset{cn}{⟶}ℂ$
cnbdibl.bd ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left|{F}\left({y}\right)\right|\le {x}$
Assertion cnbdibl ${⊢}{\phi }\to {F}\in {𝐿}^{1}$

Proof

Step Hyp Ref Expression
1 cnbdibl.a ${⊢}{\phi }\to {A}\in \mathrm{dom}vol$
2 cnbdibl.va ${⊢}{\phi }\to vol\left({A}\right)\in ℝ$
3 cnbdibl.f ${⊢}{\phi }\to {F}:{A}\underset{cn}{⟶}ℂ$
4 cnbdibl.bd ${⊢}{\phi }\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left|{F}\left({y}\right)\right|\le {x}$
5 cnmbf ${⊢}\left({A}\in \mathrm{dom}vol\wedge {F}:{A}\underset{cn}{⟶}ℂ\right)\to {F}\in MblFn$
6 1 3 5 syl2anc ${⊢}{\phi }\to {F}\in MblFn$
7 cncff ${⊢}{F}:{A}\underset{cn}{⟶}ℂ\to {F}:{A}⟶ℂ$
8 fdm ${⊢}{F}:{A}⟶ℂ\to \mathrm{dom}{F}={A}$
9 3 7 8 3syl ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
10 9 fveq2d ${⊢}{\phi }\to vol\left(\mathrm{dom}{F}\right)=vol\left({A}\right)$
11 10 2 eqeltrd ${⊢}{\phi }\to vol\left(\mathrm{dom}{F}\right)\in ℝ$
12 bddibl ${⊢}\left({F}\in MblFn\wedge vol\left(\mathrm{dom}{F}\right)\in ℝ\wedge \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{dom}{F}\phantom{\rule{.4em}{0ex}}\left|{F}\left({y}\right)\right|\le {x}\right)\to {F}\in {𝐿}^{1}$
13 6 11 4 12 syl3anc ${⊢}{\phi }\to {F}\in {𝐿}^{1}$