Metamath Proof Explorer

Theorem ibl0

Description: The zero function is integrable on any measurable set. (Unlike iblconst , this does not require A to have finite measure.) (Contributed by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion ibl0 ⊢ A ∈ dom ⁡ vol → A × 0 ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 mbfconst ⊢ A ∈ dom ⁡ vol ∧ 0 ∈ ℂ → A × 0 ∈ MblFn
3 1 2 mpan2 ⊢ A ∈ dom ⁡ vol → A × 0 ∈ MblFn
4 ax-icn ⊢ i ∈ ℂ
5 ine0 ⊢ i ≠ 0
6 elfzelz ⊢ k ∈ 0 … 3 → k ∈ ℤ
7 6 ad2antlr ⊢ A ∈ dom ⁡ vol ∧ k ∈ 0 … 3 ∧ x ∈ A → k ∈ ℤ
8 expclz ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ∈ ℂ
9 expne0i ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ≠ 0
10 8 9 div0d ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → 0 i k = 0
11 4 5 7 10 mp3an12i ⊢ A ∈ dom ⁡ vol ∧ k ∈ 0 … 3 ∧ x ∈ A → 0 i k = 0
12 11 fveq2d ⊢ A ∈ dom ⁡ vol ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ 0 i k = ℜ ⁡ 0
13 re0 ⊢ ℜ ⁡ 0 = 0
14 12 13 eqtrdi ⊢ A ∈ dom ⁡ vol ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ 0 i k = 0
15 14 itgvallem3 ⊢ A ∈ dom ⁡ vol ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0 = 0
16 0re ⊢ 0 ∈ ℝ
17 15 16 eqeltrdi ⊢ A ∈ dom ⁡ vol ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0 ∈ ℝ
18 17 ralrimiva ⊢ A ∈ dom ⁡ vol → ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0 ∈ ℝ
19 eqidd ⊢ A ∈ dom ⁡ vol → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0
20 eqidd ⊢ A ∈ dom ⁡ vol ∧ x ∈ A → ℜ ⁡ 0 i k = ℜ ⁡ 0 i k
21 c0ex ⊢ 0 ∈ V
22 21 fconst ⊢ A × 0 : A ⟶ 0
23 fdm ⊢ A × 0 : A ⟶ 0 → dom ⁡ A × 0 = A
24 22 23 mp1i ⊢ A ∈ dom ⁡ vol → dom ⁡ A × 0 = A
25 21 fvconst2 ⊢ x ∈ A → A × 0 ⁡ x = 0
26 25 adantl ⊢ A ∈ dom ⁡ vol ∧ x ∈ A → A × 0 ⁡ x = 0
27 19 20 24 26 isibl ⊢ A ∈ dom ⁡ vol → A × 0 ∈ 𝐿 1 ↔ A × 0 ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ 0 i k ℜ ⁡ 0 i k 0 ∈ ℝ
28 3 18 27 mpbir2and ⊢ A ∈ dom ⁡ vol → A × 0 ∈ 𝐿 1