Metamath Proof Explorer

Theorem ismbf

Description: The predicate " F is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl . (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion ismbf 
|- ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )

Proof

Step Hyp Ref Expression
1 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
2 fdm 
 |-  ( F : A --> RR -> dom F = A )
3 2 eleq1d 
 |-  ( F : A --> RR -> ( dom F e. dom vol <-> A e. dom vol ) )
4 1 3 syl5ib 
 |-  ( F : A --> RR -> ( F e. MblFn -> A e. dom vol ) )
5 ioomax 
 |-  ( -oo (,) +oo ) = RR
6 ioorebas 
 |-  ( -oo (,) +oo ) e. ran (,)
7 5 6 eqeltrri 
 |-  RR e. ran (,)
8 imaeq2 
 |-  ( x = RR -> ( `' F " x ) = ( `' F " RR ) )
9 8 eleq1d 
 |-  ( x = RR -> ( ( `' F " x ) e. dom vol <-> ( `' F " RR ) e. dom vol ) )
10 9 rspcv 
 |-  ( RR e. ran (,) -> ( A. x e. ran (,) ( `' F " x ) e. dom vol -> ( `' F " RR ) e. dom vol ) )
11 7 10 ax-mp 
 |-  ( A. x e. ran (,) ( `' F " x ) e. dom vol -> ( `' F " RR ) e. dom vol )
12 fimacnv 
 |-  ( F : A --> RR -> ( `' F " RR ) = A )
13 12 eleq1d 
 |-  ( F : A --> RR -> ( ( `' F " RR ) e. dom vol <-> A e. dom vol ) )
14 11 13 syl5ib 
 |-  ( F : A --> RR -> ( A. x e. ran (,) ( `' F " x ) e. dom vol -> A e. dom vol ) )
15 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 ) ) )
16 ffvelrn 
 |-  ( ( F : A --> RR /\ x e. A ) -> ( F ` x ) e. RR )
17 16 adantlr 
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( F ` x ) e. RR )
18 17 rered 
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( Re ` ( F ` x ) ) = ( F ` x ) )
19 18 mpteq2dva 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( x e. A |-> ( Re ` ( F ` x ) ) ) = ( x e. A |-> ( F ` x ) ) )
20 17 recnd 
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( F ` x ) e. CC )
21 simpl 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F : A --> RR )
22 21 feqmptd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F = ( x e. A |-> ( F ` x ) ) )
23 ref 
 |-  Re : CC --> RR
24 23 a1i 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Re : CC --> RR )
25 24 feqmptd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Re = ( y e. CC |-> ( Re ` y ) ) )
26 fveq2 
 |-  ( y = ( F ` x ) -> ( Re ` y ) = ( Re ` ( F ` x ) ) )
27 20 22 25 26 fmptco 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Re o. F ) = ( x e. A |-> ( Re ` ( F ` x ) ) ) )
28 19 27 22 3eqtr4rd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F = ( Re o. F ) )
29 28 cnveqd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> `' F = `' ( Re o. F ) )
30 29 imaeq1d 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' F " x ) = ( `' ( Re o. F ) " x ) )
31 30 eleq1d 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' F " x ) e. dom vol <-> ( `' ( Re o. F ) " x ) e. dom vol ) )
32 imf 
 |-  Im : CC --> RR
33 32 a1i 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Im : CC --> RR )
34 33 feqmptd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Im = ( y e. CC |-> ( Im ` y ) ) )
35 fveq2 
 |-  ( y = ( F ` x ) -> ( Im ` y ) = ( Im ` ( F ` x ) ) )
36 20 22 34 35 fmptco 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( x e. A |-> ( Im ` ( F ` x ) ) ) )
37 17 reim0d 
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( Im ` ( F ` x ) ) = 0 )
38 37 mpteq2dva 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( x e. A |-> ( Im ` ( F ` x ) ) ) = ( x e. A |-> 0 ) )
39 36 38 eqtrd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( x e. A |-> 0 ) )
40 fconstmpt 
 |-  ( A X. { 0 } ) = ( x e. A |-> 0 )
41 39 40 eqtr4di 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( A X. { 0 } ) )
42 41 cnveqd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> `' ( Im o. F ) = `' ( A X. { 0 } ) )
43 42 imaeq1d 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( Im o. F ) " x ) = ( `' ( A X. { 0 } ) " x ) )
44 simpr 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> A e. dom vol )
45 0re 
 |-  0 e. RR
46 mbfconstlem 
 |-  ( ( A e. dom vol /\ 0 e. RR ) -> ( `' ( A X. { 0 } ) " x ) e. dom vol )
47 44 45 46 sylancl 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( A X. { 0 } ) " x ) e. dom vol )
48 43 47 eqeltrd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( Im o. F ) " x ) e. dom vol )
49 48 biantrud 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' ( Re o. F ) " x ) e. dom vol <-> ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
50 31 49 bitrd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' F " x ) e. dom vol <-> ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
51 50 ralbidv 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( A. x e. ran (,) ( `' F " x ) e. dom vol <-> A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
52 ax-resscn 
 |-  RR C_ CC
53 fss 
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
54 52 53 mpan2 
 |-  ( F : A --> RR -> F : A --> CC )
55 mblss 
 |-  ( A e. dom vol -> A C_ RR )
56 cnex 
 |-  CC e. _V
57 reex 
 |-  RR e. _V
58 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
59 56 57 58 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
60 54 55 59 syl2an 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F e. ( CC ^pm RR ) )
61 60 biantrurd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) ) )
62 51 61 bitrd 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( A. x e. ran (,) ( `' F " x ) e. dom vol <-> ( F e. ( CC ^pm RR ) /\ A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) ) )
63 15 62 bitr4id 
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
64 63 ex 
 |-  ( F : A --> RR -> ( A e. dom vol -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) ) )
65 4 14 64 pm5.21ndd 
 |-  ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )