Metamath Proof Explorer

Theorem bddibl

Description: A bounded function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion bddibl ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
2 1 3ad2ant1 ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → dom 𝐹 ∈ dom vol )
3 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
4 3 3ad2ant1 ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 : dom 𝐹 ⟶ ℂ )
5 4 ffnd ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 Fn dom 𝐹 )
6 1cnd ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 1 ∈ ℂ )
7 fnconstg ⊢ ( 1 ∈ ℂ → ( dom 𝐹 × { 1 } ) Fn dom 𝐹 )
8 6 7 syl ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( dom 𝐹 × { 1 } ) Fn dom 𝐹 )
9 eqidd ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
10 1ex ⊢ 1 ∈ V
11 10 fvconst2 ⊢ ( 𝑧 ∈ dom 𝐹 → ( ( dom 𝐹 × { 1 } ) ‘ 𝑧 ) = 1 )
12 11 adantl ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( dom 𝐹 × { 1 } ) ‘ 𝑧 ) = 1 )
13 4 ffvelrnda ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑧 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
14 13 mulid1d ⊢ ( ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) · 1 ) = ( 𝐹 ‘ 𝑧 ) )
15 2 5 8 5 9 12 14 offveq ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · ( dom 𝐹 × { 1 } ) ) = 𝐹 )
16 simp2 ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( vol ‘ dom 𝐹 ) ∈ ℝ )
17 iblconst ⊢ ( ( dom 𝐹 ∈ dom vol ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ 1 ∈ ℂ ) → ( dom 𝐹 × { 1 } ) ∈ 𝐿1 )
18 2 16 6 17 syl3anc ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( dom 𝐹 × { 1 } ) ∈ 𝐿1 )
19 bddmulibl ⊢ ( ( 𝐹 ∈ MblFn ∧ ( dom 𝐹 × { 1 } ) ∈ 𝐿1 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · ( dom 𝐹 × { 1 } ) ) ∈ 𝐿1 )
20 18 19 syld3an2 ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → ( 𝐹 ∘f · ( dom 𝐹 × { 1 } ) ) ∈ 𝐿1 )
21 15 20 eqeltrrd ⊢ ( ( 𝐹 ∈ MblFn ∧ ( vol ‘ dom 𝐹 ) ∈ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ dom 𝐹 ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑥 ) → 𝐹 ∈ 𝐿1 )