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 ffvelrn
 |-  ( ( F : A --> RR /\ x e. A ) -> ( F ` x ) e. RR )
16 15 adantlr
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( F ` x ) e. RR )
17 16 rered
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( Re ` ( F ` x ) ) = ( F ` x ) )
18 17 mpteq2dva
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( x e. A |-> ( Re ` ( F ` x ) ) ) = ( x e. A |-> ( F ` x ) ) )
19 16 recnd
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( F ` x ) e. CC )
20 simpl
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F : A --> RR )
21 20 feqmptd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F = ( x e. A |-> ( F ` x ) ) )
22 ref
 |-  Re : CC --> RR
23 22 a1i
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Re : CC --> RR )
24 23 feqmptd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Re = ( y e. CC |-> ( Re ` y ) ) )
25 fveq2
 |-  ( y = ( F ` x ) -> ( Re ` y ) = ( Re ` ( F ` x ) ) )
26 19 21 24 25 fmptco
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Re o. F ) = ( x e. A |-> ( Re ` ( F ` x ) ) ) )
27 18 26 21 3eqtr4rd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F = ( Re o. F ) )
28 27 cnveqd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> `' F = `' ( Re o. F ) )
29 28 imaeq1d
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' F " x ) = ( `' ( Re o. F ) " x ) )
30 29 eleq1d
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( ( `' F " x ) e. dom vol <-> ( `' ( Re o. F ) " x ) e. dom vol ) )
31 imf
 |-  Im : CC --> RR
32 31 a1i
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Im : CC --> RR )
33 32 feqmptd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> Im = ( y e. CC |-> ( Im ` y ) ) )
34 fveq2
 |-  ( y = ( F ` x ) -> ( Im ` y ) = ( Im ` ( F ` x ) ) )
35 19 21 33 34 fmptco
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( x e. A |-> ( Im ` ( F ` x ) ) ) )
36 16 reim0d
 |-  ( ( ( F : A --> RR /\ A e. dom vol ) /\ x e. A ) -> ( Im ` ( F ` x ) ) = 0 )
37 36 mpteq2dva
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( x e. A |-> ( Im ` ( F ` x ) ) ) = ( x e. A |-> 0 ) )
38 35 37 eqtrd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( x e. A |-> 0 ) )
39 fconstmpt
 |-  ( A X. { 0 } ) = ( x e. A |-> 0 )
40 38 39 syl6eqr
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( Im o. F ) = ( A X. { 0 } ) )
41 40 cnveqd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> `' ( Im o. F ) = `' ( A X. { 0 } ) )
42 41 imaeq1d
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( Im o. F ) " x ) = ( `' ( A X. { 0 } ) " x ) )
43 simpr
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> A e. dom vol )
44 0re
 |-  0 e. RR
45 mbfconstlem
 |-  ( ( A e. dom vol /\ 0 e. RR ) -> ( `' ( A X. { 0 } ) " x ) e. dom vol )
46 43 44 45 sylancl
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( A X. { 0 } ) " x ) e. dom vol )
47 42 46 eqeltrd
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> ( `' ( Im o. F ) " x ) e. dom vol )
48 47 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 ) ) )
49 30 48 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 ) ) )
50 49 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 ) ) )
51 ax-resscn
 |-  RR C_ CC
52 fss
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
53 51 52 mpan2
 |-  ( F : A --> RR -> F : A --> CC )
54 mblss
 |-  ( A e. dom vol -> A C_ RR )
55 cnex
 |-  CC e. _V
56 reex
 |-  RR e. _V
57 elpm2r
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
58 55 56 57 mpanl12
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
59 53 54 58 syl2an
 |-  ( ( F : A --> RR /\ A e. dom vol ) -> F e. ( CC ^pm RR ) )
60 59 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 ) ) ) )
61 50 60 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 ) ) ) )
62 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 ) ) )
63 61 62 syl6rbbr
 |-  ( ( 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 ) )