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

Theorem isibl 25212
Description: The predicate "𝐹 is integrable". The "integrable" predicate corresponds roughly to the range of validity of 𝐴𝐵 d𝑥, which is to say that the expression 𝐴𝐵 d𝑥 doesn't make sense unless (𝑥𝐴𝐵) ∈ 𝐿1. (Contributed by Mario Carneiro, 28-Jun-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
isibl.1 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
isibl.2 ((𝜑𝑥𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))))
isibl.3 (𝜑 → dom 𝐹 = 𝐴)
isibl.4 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
Assertion
Ref Expression
isibl (𝜑 → (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2𝐺) ∈ ℝ)))
Distinct variable groups:   𝑥,𝑘,𝐴   𝐵,𝑘   𝑘,𝐹,𝑥   𝜑,𝑘,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝑇(𝑥,𝑘)   𝐺(𝑥,𝑘)

Proof of Theorem isibl
Dummy variables 𝑓 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6891 . . . . . . . . 9 (ℜ‘((𝑓𝑥) / (i↑𝑘))) ∈ V
2 breq2 5145 . . . . . . . . . . 11 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → (0 ≤ 𝑦 ↔ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))))
32anbi2d 629 . . . . . . . . . 10 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → ((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦) ↔ (𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘))))))
4 id 22 . . . . . . . . . 10 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → 𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))))
53, 4ifbieq1d 4546 . . . . . . . . 9 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0))
61, 5csbie 3925 . . . . . . . 8 (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0)
7 dmeq 5895 . . . . . . . . . . 11 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
87eleq2d 2818 . . . . . . . . . 10 (𝑓 = 𝐹 → (𝑥 ∈ dom 𝑓𝑥 ∈ dom 𝐹))
9 fveq1 6877 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
109fvoveq1d 7415 . . . . . . . . . . 11 (𝑓 = 𝐹 → (ℜ‘((𝑓𝑥) / (i↑𝑘))) = (ℜ‘((𝐹𝑥) / (i↑𝑘))))
1110breq2d 5153 . . . . . . . . . 10 (𝑓 = 𝐹 → (0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘))) ↔ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))))
128, 11anbi12d 631 . . . . . . . . 9 (𝑓 = 𝐹 → ((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))) ↔ (𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘))))))
1312, 10ifbieq1d 4546 . . . . . . . 8 (𝑓 = 𝐹 → if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0) = if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
146, 13eqtrid 2783 . . . . . . 7 (𝑓 = 𝐹(ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
1514mpteq2dv 5243 . . . . . 6 (𝑓 = 𝐹 → (𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)))
1615fveq2d 6882 . . . . 5 (𝑓 = 𝐹 → (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))))
1716eleq1d 2817 . . . 4 (𝑓 = 𝐹 → ((∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
1817ralbidv 3176 . . 3 (𝑓 = 𝐹 → (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ ↔ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
19 df-ibl 25068 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2018, 19elrab2 3682 . 2 (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
21 isibl.3 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐴)
2221eleq2d 2818 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ dom 𝐹𝑥𝐴))
2322anbi1d 630 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))) ↔ (𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘))))))
2423ifbid 4545 . . . . . . . . 9 (𝜑 → if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
25 isibl.4 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
2625fvoveq1d 7415 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (ℜ‘((𝐹𝑥) / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
27 isibl.2 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))))
2826, 27eqtr4d 2774 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (ℜ‘((𝐹𝑥) / (i↑𝑘))) = 𝑇)
2928ibllem 25211 . . . . . . . . 9 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))
3024, 29eqtrd 2771 . . . . . . . 8 (𝜑 → if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))
3130mpteq2dv 5243 . . . . . . 7 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
32 isibl.1 . . . . . . 7 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
3331, 32eqtr4d 2774 . . . . . 6 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)) = 𝐺)
3433fveq2d 6882 . . . . 5 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) = (∫2𝐺))
3534eleq1d 2817 . . . 4 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2𝐺) ∈ ℝ))
3635ralbidv 3176 . . 3 (𝜑 → (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ ↔ ∀𝑘 ∈ (0...3)(∫2𝐺) ∈ ℝ))
3736anbi2d 629 . 2 (𝜑 → ((𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ) ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2𝐺) ∈ ℝ)))
3820, 37bitrid 282 1 (𝜑 → (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2𝐺) ∈ ℝ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3060  csb 3889  ifcif 4522   class class class wbr 5141  cmpt 5224  dom cdm 5669  cfv 6532  (class class class)co 7393  cr 11091  0cc0 11092  ici 11094  cle 11231   / cdiv 11853  3c3 12250  ...cfz 13466  cexp 14009  cre 15026  MblFncmbf 25060  2citg2 25062  𝐿1cibl 25063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5299
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-br 5142  df-opab 5204  df-mpt 5225  df-dm 5679  df-iota 6484  df-fv 6540  df-ov 7396  df-ibl 25068
This theorem is referenced by:  isibl2  25213  ibl0  25233  iblempty  44454
  Copyright terms: Public domain W3C validator