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

Theorem isibl 25130
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 6855 . . . . . . . . 9 (ℜ‘((𝑓𝑥) / (i↑𝑘))) ∈ V
2 breq2 5109 . . . . . . . . . . 11 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → (0 ≤ 𝑦 ↔ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))))
32anbi2d 629 . . . . . . . . . 10 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → ((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦) ↔ (𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘))))))
4 id 22 . . . . . . . . . 10 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → 𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))))
53, 4ifbieq1d 4510 . . . . . . . . 9 (𝑦 = (ℜ‘((𝑓𝑥) / (i↑𝑘))) → if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0))
61, 5csbie 3891 . . . . . . . 8 (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0)
7 dmeq 5859 . . . . . . . . . . 11 (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
87eleq2d 2823 . . . . . . . . . 10 (𝑓 = 𝐹 → (𝑥 ∈ dom 𝑓𝑥 ∈ dom 𝐹))
9 fveq1 6841 . . . . . . . . . . . 12 (𝑓 = 𝐹 → (𝑓𝑥) = (𝐹𝑥))
109fvoveq1d 7379 . . . . . . . . . . 11 (𝑓 = 𝐹 → (ℜ‘((𝑓𝑥) / (i↑𝑘))) = (ℜ‘((𝐹𝑥) / (i↑𝑘))))
1110breq2d 5117 . . . . . . . . . 10 (𝑓 = 𝐹 → (0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘))) ↔ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))))
128, 11anbi12d 631 . . . . . . . . 9 (𝑓 = 𝐹 → ((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))) ↔ (𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘))))))
1312, 10ifbieq1d 4510 . . . . . . . 8 (𝑓 = 𝐹 → if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ (ℜ‘((𝑓𝑥) / (i↑𝑘)))), (ℜ‘((𝑓𝑥) / (i↑𝑘))), 0) = if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
146, 13eqtrid 2788 . . . . . . 7 (𝑓 = 𝐹(ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0) = if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
1514mpteq2dv 5207 . . . . . 6 (𝑓 = 𝐹 → (𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)))
1615fveq2d 6846 . . . . 5 (𝑓 = 𝐹 → (∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) = (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))))
1716eleq1d 2822 . . . 4 (𝑓 = 𝐹 → ((∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ ↔ (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
1817ralbidv 3174 . . 3 (𝑓 = 𝐹 → (∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ ↔ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
19 df-ibl 24986 . . 3 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ (ℜ‘((𝑓𝑥) / (i↑𝑘))) / 𝑦if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
2018, 19elrab2 3648 . 2 (𝐹 ∈ 𝐿1 ↔ (𝐹 ∈ MblFn ∧ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ))
21 isibl.3 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = 𝐴)
2221eleq2d 2823 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ dom 𝐹𝑥𝐴))
2322anbi1d 630 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))) ↔ (𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘))))))
2423ifbid 4509 . . . . . . . . 9 (𝜑 → if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))
25 isibl.4 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → (𝐹𝑥) = 𝐵)
2625fvoveq1d 7379 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → (ℜ‘((𝐹𝑥) / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘))))
27 isibl.2 . . . . . . . . . . 11 ((𝜑𝑥𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝑘))))
2826, 27eqtr4d 2779 . . . . . . . . . 10 ((𝜑𝑥𝐴) → (ℜ‘((𝐹𝑥) / (i↑𝑘))) = 𝑇)
2928ibllem 25129 . . . . . . . . 9 (𝜑 → if((𝑥𝐴 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))
3024, 29eqtrd 2776 . . . . . . . 8 (𝜑 → if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0) = if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))
3130mpteq2dv 5207 . . . . . . 7 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
32 isibl.1 . . . . . . 7 (𝜑𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)))
3331, 32eqtr4d 2779 . . . . . 6 (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0)) = 𝐺)
3433fveq2d 6846 . . . . 5 (𝜑 → (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) = (∫2𝐺))
3534eleq1d 2822 . . . 4 (𝜑 → ((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ dom 𝐹 ∧ 0 ≤ (ℜ‘((𝐹𝑥) / (i↑𝑘)))), (ℜ‘((𝐹𝑥) / (i↑𝑘))), 0))) ∈ ℝ ↔ (∫2𝐺) ∈ ℝ))
3635ralbidv 3174 . . 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 3064  csb 3855  ifcif 4486   class class class wbr 5105  cmpt 5188  dom cdm 5633  cfv 6496  (class class class)co 7357  cr 11050  0cc0 11051  ici 11053  cle 11190   / cdiv 11812  3c3 12209  ...cfz 13424  cexp 13967  cre 14982  MblFncmbf 24978  2citg2 24980  𝐿1cibl 24981
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 2707  ax-nul 5263
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 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-dm 5643  df-iota 6448  df-fv 6504  df-ov 7360  df-ibl 24986
This theorem is referenced by:  isibl2  25131  ibl0  25151  iblempty  44196
  Copyright terms: Public domain W3C validator