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

Theorem ismbf1 24231
Description: The predicate "𝐹 is a measurable function". This is more naturally stated for functions on the reals, see ismbf 24235 and ismbfcn 24236 for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014.)
Assertion
Ref Expression
ismbf1 (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
Distinct variable group:   𝑥,𝐹

Proof of Theorem ismbf1
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 coeq2 5697 . . . . . . 7 (𝑓 = 𝐹 → (ℜ ∘ 𝑓) = (ℜ ∘ 𝐹))
21cnveqd 5714 . . . . . 6 (𝑓 = 𝐹(ℜ ∘ 𝑓) = (ℜ ∘ 𝐹))
32imaeq1d 5899 . . . . 5 (𝑓 = 𝐹 → ((ℜ ∘ 𝑓) “ 𝑥) = ((ℜ ∘ 𝐹) “ 𝑥))
43eleq1d 2877 . . . 4 (𝑓 = 𝐹 → (((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ↔ ((ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol))
5 coeq2 5697 . . . . . . 7 (𝑓 = 𝐹 → (ℑ ∘ 𝑓) = (ℑ ∘ 𝐹))
65cnveqd 5714 . . . . . 6 (𝑓 = 𝐹(ℑ ∘ 𝑓) = (ℑ ∘ 𝐹))
76imaeq1d 5899 . . . . 5 (𝑓 = 𝐹 → ((ℑ ∘ 𝑓) “ 𝑥) = ((ℑ ∘ 𝐹) “ 𝑥))
87eleq1d 2877 . . . 4 (𝑓 = 𝐹 → (((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol ↔ ((ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))
94, 8anbi12d 633 . . 3 (𝑓 = 𝐹 → ((((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol) ↔ (((ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
109ralbidv 3165 . 2 (𝑓 = 𝐹 → (∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol) ↔ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
11 df-mbf 24226 . 2 MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
1210, 11elrab2 3634 1 (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)(((ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ ((ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399   = wceq 1538  wcel 2112  wral 3109  ccnv 5522  dom cdm 5523  ran crn 5524  cima 5526  ccom 5527  (class class class)co 7139  pm cpm 8394  cc 10528  cr 10529  (,)cioo 12730  cre 14451  cim 14452  volcvol 24070  MblFncmbf 24221
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rab 3118  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-mbf 24226
This theorem is referenced by:  mbff  24232  mbfdm  24233  ismbf  24235  ismbfcn  24236  mbfconst  24240  mbfres  24251  cncombf  24265  cnmbf  24266  mbfdmssre  42629
  Copyright terms: Public domain W3C validator