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

Theorem ismbf1 21238
Description: The predicate " F is a measurable function". This is more naturally stated for functions on the reals, see ismbf 21242 and ismbfcn 21243 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 5107 . . . . . . 7  |-  ( f  =  F  ->  (
Re  o.  f )  =  ( Re  o.  F ) )
21cnveqd 5124 . . . . . 6  |-  ( f  =  F  ->  `' ( Re  o.  f
)  =  `' ( Re  o.  F ) )
32imaeq1d 5277 . . . . 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 5107 . . . . . . 7  |-  ( f  =  F  ->  (
Im  o.  f )  =  ( Im  o.  F ) )
65cnveqd 5124 . . . . . 6  |-  ( f  =  F  ->  `' ( Im  o.  f
)  =  `' ( Im  o.  F ) )
76imaeq1d 5277 . . . . 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 710 . . 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 2846 . 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 21233 . 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 3226 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 369    = wceq 1370    e. wcel 1758   A.wral 2799   `'ccnv 4948   dom cdm 4949   ran crn 4950   "cima 4952    o. ccom 4953  (class class class)co 6201    ^pm cpm 7326   CCcc 9392   RRcr 9393   (,)cioo 11412   Recre 12705   Imcim 12706   volcvol 21080  MblFncmbf 21228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-br 4402  df-opab 4460  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-mbf 21233
This theorem is referenced by:  mbff  21239  mbfdm  21240  ismbf  21242  ismbfcn  21243  mbfconst  21247  mbfres  21256  cncombf  21270  cnmbf  21271
  Copyright terms: Public domain W3C validator