Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ibl Structured version   Visualization version   GIF version

Definition df-ibl 23582
 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.)
Assertion
Ref Expression
df-ibl 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
Distinct variable group:   𝑦,𝑘,𝑓,𝑥

Detailed syntax breakdown of Definition df-ibl
StepHypRef Expression
1 cibl 23577 . 2 class 𝐿1
2 vx . . . . . . 7 setvar 𝑥
3 cr 10119 . . . . . . 7 class
4 vy . . . . . . . 8 setvar 𝑦
52cv 1623 . . . . . . . . . . 11 class 𝑥
6 vf . . . . . . . . . . . 12 setvar 𝑓
76cv 1623 . . . . . . . . . . 11 class 𝑓
85, 7cfv 6041 . . . . . . . . . 10 class (𝑓𝑥)
9 ci 10122 . . . . . . . . . . 11 class i
10 vk . . . . . . . . . . . 12 setvar 𝑘
1110cv 1623 . . . . . . . . . . 11 class 𝑘
12 cexp 13046 . . . . . . . . . . 11 class
139, 11, 12co 6805 . . . . . . . . . 10 class (i↑𝑘)
14 cdiv 10868 . . . . . . . . . 10 class /
158, 13, 14co 6805 . . . . . . . . 9 class ((𝑓𝑥) / (i↑𝑘))
16 cre 14028 . . . . . . . . 9 class
1715, 16cfv 6041 . . . . . . . 8 class (ℜ‘((𝑓𝑥) / (i↑𝑘)))
187cdm 5258 . . . . . . . . . . 11 class dom 𝑓
195, 18wcel 2131 . . . . . . . . . 10 wff 𝑥 ∈ dom 𝑓
20 cc0 10120 . . . . . . . . . . 11 class 0
214cv 1623 . . . . . . . . . . 11 class 𝑦
22 cle 10259 . . . . . . . . . . 11 class
2320, 21, 22wbr 4796 . . . . . . . . . 10 wff 0 ≤ 𝑦
2419, 23wa 383 . . . . . . . . 9 wff (𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦)
2524, 21, 20cif 4222 . . . . . . . 8 class if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
264, 17, 25csb 3666 . . . . . . 7 class (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
272, 3, 26cmpt 4873 . . . . . 6 class (𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))
28 citg2 23576 . . . . . 6 class 2
2927, 28cfv 6041 . . . . 5 class (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)))
3029, 3wcel 2131 . . . 4 wff (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
31 c3 11255 . . . . 5 class 3
32 cfz 12511 . . . . 5 class ...
3320, 31, 32co 6805 . . . 4 class (0...3)
3430, 10, 33wral 3042 . . 3 wff 𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
35 cmbf 23574 . . 3 class MblFn
3634, 6, 35crab 3046 . 2 class {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
371, 36wceq 1624 1 wff 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
 Colors of variables: wff setvar class This definition is referenced by:  isibl  23723  iblmbf  23725
 Copyright terms: Public domain W3C validator