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

Theorem ismbf1 22199
Description: The predicate " F is a measurable function". This is more naturally stated for functions on the reals, see ismbf 22203 and ismbfcn 22204 for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014.)
Assertion
Ref Expression
ismbf1  |-  ( F  e. MblFn 
<->  ( F  e.  ( CC  ^pm  RR )  /\  A. x  e.  ran  (,) ( ( `' ( Re  o.  F )
" x )  e. 
dom  vol  /\  ( `' ( Im  o.  F
) " x )  e.  dom  vol )
) )
Distinct variable group:    x, F

Proof of Theorem ismbf1
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 coeq2 5150 . . . . . . 7  |-  ( f  =  F  ->  (
Re  o.  f )  =  ( Re  o.  F ) )
21cnveqd 5167 . . . . . 6  |-  ( f  =  F  ->  `' ( Re  o.  f
)  =  `' ( Re  o.  F ) )
32imaeq1d 5324 . . . . 5  |-  ( f  =  F  ->  ( `' ( Re  o.  f ) " x
)  =  ( `' ( Re  o.  F
) " x ) )
43eleq1d 2523 . . . 4  |-  ( f  =  F  ->  (
( `' ( Re  o.  f ) "
x )  e.  dom  vol  <->  ( `' ( Re  o.  F ) " x
)  e.  dom  vol ) )
5 coeq2 5150 . . . . . . 7  |-  ( f  =  F  ->  (
Im  o.  f )  =  ( Im  o.  F ) )
65cnveqd 5167 . . . . . 6  |-  ( f  =  F  ->  `' ( Im  o.  f
)  =  `' ( Im  o.  F ) )
76imaeq1d 5324 . . . . 5  |-  ( f  =  F  ->  ( `' ( Im  o.  f ) " x
)  =  ( `' ( Im  o.  F
) " x ) )
87eleq1d 2523 . . . 4  |-  ( f  =  F  ->  (
( `' ( Im  o.  f ) "
x )  e.  dom  vol  <->  ( `' ( Im  o.  F ) " x
)  e.  dom  vol ) )
94, 8anbi12d 708 . . 3  |-  ( f  =  F  ->  (
( ( `' ( Re  o.  f )
" x )  e. 
dom  vol  /\  ( `' ( Im  o.  f
) " x )  e.  dom  vol )  <->  ( ( `' ( Re  o.  F ) "
x )  e.  dom  vol 
/\  ( `' ( Im  o.  F )
" x )  e. 
dom  vol ) ) )
109ralbidv 2893 . 2  |-  ( f  =  F  ->  ( A. x  e.  ran  (,) ( ( `' ( Re  o.  f )
" x )  e. 
dom  vol  /\  ( `' ( Im  o.  f
) " x )  e.  dom  vol )  <->  A. x  e.  ran  (,) ( ( `' ( Re  o.  F )
" x )  e. 
dom  vol  /\  ( `' ( Im  o.  F
) " x )  e.  dom  vol )
) )
11 df-mbf 22194 . 2  |- MblFn  =  {
f  e.  ( CC 
^pm  RR )  |  A. x  e.  ran  (,) (
( `' ( Re  o.  f ) "
x )  e.  dom  vol 
/\  ( `' ( Im  o.  f )
" x )  e. 
dom  vol ) }
1210, 11elrab2 3256 1  |-  ( F  e. MblFn 
<->  ( F  e.  ( CC  ^pm  RR )  /\  A. x  e.  ran  (,) ( ( `' ( Re  o.  F )
" x )  e. 
dom  vol  /\  ( `' ( Im  o.  F
) " x )  e.  dom  vol )
) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    = wceq 1398    e. wcel 1823   A.wral 2804   `'ccnv 4987   dom cdm 4988   ran crn 4989   "cima 4991    o. ccom 4992  (class class class)co 6270    ^pm cpm 7413   CCcc 9479   RRcr 9480   (,)cioo 11532   Recre 13012   Imcim 13013   volcvol 22041  MblFncmbf 22189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-mbf 22194
This theorem is referenced by:  mbff  22200  mbfdm  22201  ismbf  22203  ismbfcn  22204  mbfconst  22208  mbfres  22217  cncombf  22231  cnmbf  22232
  Copyright terms: Public domain W3C validator