Metamath Proof Explorer

Definition df-ibl

Description: Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion df-ibl ⊢ 𝐿 1 = f ∈ MblFn | ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ

Detailed syntax breakdown

Step Hyp Ref Expression
0 cibl class 𝐿 1
1 vf setvar f
2 cmbf class MblFn
3 vk setvar k
4 cc0 class 0
5 cfz class …
6 c3 class 3
7 4 6 5 co class 0 … 3
8 citg2 class ∫ 2
9 vx setvar x
10 cr class ℝ
11 cre class ℜ
12 1 cv setvar f
13 9 cv setvar x
14 13 12 cfv class f ⁡ x
15 cdiv class ÷
16 ci class i
17 cexp class ^
18 3 cv setvar k
19 16 18 17 co class i k
20 14 19 15 co class f ⁡ x i k
21 20 11 cfv class ℜ ⁡ f ⁡ x i k
22 vy setvar y
23 12 cdm class dom ⁡ f
24 13 23 wcel wff x ∈ dom ⁡ f
25 cle class ≤
26 22 cv setvar y
27 4 26 25 wbr wff 0 ≤ y
28 24 27 wa wff x ∈ dom ⁡ f ∧ 0 ≤ y
29 28 26 4 cif class if x ∈ dom ⁡ f ∧ 0 ≤ y y 0
30 22 21 29 csb class ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0
31 9 10 30 cmpt class x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0
32 31 8 cfv class ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0
33 32 10 wcel wff ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ
34 33 3 7 wral wff ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ
35 34 1 2 crab class f ∈ MblFn | ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ
36 0 35 wceq wff 𝐿 1 = f ∈ MblFn | ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ ⦋ ℜ ⁡ f ⁡ x i k / y⦌ if x ∈ dom ⁡ f ∧ 0 ≤ y y 0 ∈ ℝ