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

Theorem isibl 25820
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 6933 . . . . . . . . 9 (ℜ‘((𝑓𝑥) / (i↑𝑘))) ∈ V
2 breq2 5170 . . . . . . . . . . 11 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → (0 ≤ 𝑦 ↔ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))))
32anbi2d 629 . . . . . . . . . 10 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → ((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦) ↔ (𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘))))))
4 id 22 . . . . . . . . . 10 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → 𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))))
53, 4ifbieq1d 4572 . . . . . . . . 9 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0))
61, 5csbie 3957 . . . . . . . 8 (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0)
7 dmeq 5928 . . . . . . . . . . 11 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
87eleq2d 2830 . . . . . . . . . 10 (𝑓 = 𝐹 → (𝑥 ∈ dom 𝑓𝑥 ∈ dom 𝐹))
9 fveq1 6919 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
109fvoveq1d 7470 . . . . . . . . . . 11 (𝑓 = 𝐹 → (ℜ‘((𝑓𝑥) / (i↑𝑘))) = (ℜ‘((𝐹𝑥) / (i↑𝑘))))
1110breq2d 5178 . . . . . . . . . 10 (𝑓 = 𝐹 → (0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘))) ↔ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))))
128, 11anbi12d 631 . . . . . . . . 9 (𝑓 = 𝐹 → ((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))) ↔ (𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘))))))
1312, 10ifbieq1d 4572 . . . . . . . 8 (𝑓 = 𝐹 → if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0) = if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
146, 13eqtrid 2792 . . . . . . 7 (𝑓 = 𝐹(ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
1514mpteq2dv 5268 . . . . . 6 (𝑓 = 𝐹 → (𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)))
1615fveq2d 6924 . . . . 5 (𝑓 = 𝐹 → (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))))
1716eleq1d 2829 . . . 4 (𝑓 = 𝐹 → ((∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
1817ralbidv 3184 . . 3 (𝑓 = 𝐹 → (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ ↔ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
19 df-ibl 25676 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2018, 19elrab2 3711 . 2 (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
21 isibl.3 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐴)
2221eleq2d 2830 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ dom 𝐹𝑥𝐴))
2322anbi1d 630 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))) ↔ (𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘))))))
2423ifbid 4571 . . . . . . . . 9 (𝜑 → if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
25 isibl.4 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
2625fvoveq1d 7470 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (ℜ‘((𝐹𝑥) / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
27 isibl.2 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))))
2826, 27eqtr4d 2783 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (ℜ‘((𝐹𝑥) / (i↑𝑘))) = 𝑇)
2928ibllem 25819 . . . . . . . . 9 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))
3024, 29eqtrd 2780 . . . . . . . 8 (𝜑 → if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))
3130mpteq2dv 5268 . . . . . . 7 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
32 isibl.1 . . . . . . 7 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
3331, 32eqtr4d 2783 . . . . . 6 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)) = 𝐺)
3433fveq2d 6924 . . . . 5 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) = (∫2𝐺))
3534eleq1d 2829 . . . 4 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2𝐺) ∈ ℝ))
3635ralbidv 3184 . . 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 283 1 (𝜑 → (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2𝐺) ∈ ℝ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2108  wral 3067  csb 3921  ifcif 4548   class class class wbr 5166  cmpt 5249  dom cdm 5700  cfv 6573  (class class class)co 7448  cr 11183  0cc0 11184  ici 11186  cle 11325   / cdiv 11947  3c3 12349  ...cfz 13567  cexp 14112  cre 15146  MblFncmbf 25668  2citg2 25670  𝐿1cibl 25671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-dm 5710  df-iota 6525  df-fv 6581  df-ov 7451  df-ibl 25676
This theorem is referenced by:  isibl2  25821  ibl0  25842  iblempty  45886
  Copyright terms: Public domain W3C validator