Metamath Proof Explorer

Theorem mbfres

Description: The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion mbfres 
|- ( ( F e. MblFn /\ A e. dom vol ) -> ( F |` A ) e. MblFn )

Proof

Step Hyp Ref Expression
1 ref 
 |-  Re : CC --> RR
2 simpr 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> A e. dom vol )
3 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 ) ) )
4 3 simplbi 
 |-  ( F e. MblFn -> F e. ( CC ^pm RR ) )
5 4 adantr 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> F e. ( CC ^pm RR ) )
6 pmresg 
 |-  ( ( A e. dom vol /\ F e. ( CC ^pm RR ) ) -> ( F |` A ) e. ( CC ^pm A ) )
7 2 5 6 syl2anc 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( F |` A ) e. ( CC ^pm A ) )
8 cnex 
 |-  CC e. _V
9 elpm2g 
 |-  ( ( CC e. _V /\ A e. dom vol ) -> ( ( F |` A ) e. ( CC ^pm A ) <-> ( ( F |` A ) : dom ( F |` A ) --> CC /\ dom ( F |` A ) C_ A ) ) )
10 8 2 9 sylancr 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( F |` A ) e. ( CC ^pm A ) <-> ( ( F |` A ) : dom ( F |` A ) --> CC /\ dom ( F |` A ) C_ A ) ) )
11 7 10 mpbid 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( F |` A ) : dom ( F |` A ) --> CC /\ dom ( F |` A ) C_ A ) )
12 11 simpld 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( F |` A ) : dom ( F |` A ) --> CC )
13 fco 
 |-  ( ( Re : CC --> RR /\ ( F |` A ) : dom ( F |` A ) --> CC ) -> ( Re o. ( F |` A ) ) : dom ( F |` A ) --> RR )
14 1 12 13 sylancr 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( Re o. ( F |` A ) ) : dom ( F |` A ) --> RR )
15 dmres 
 |-  dom ( F |` A ) = ( A i^i dom F )
16 id 
 |-  ( A e. dom vol -> A e. dom vol )
17 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
18 inmbl 
 |-  ( ( A e. dom vol /\ dom F e. dom vol ) -> ( A i^i dom F ) e. dom vol )
19 16 17 18 syl2anr 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( A i^i dom F ) e. dom vol )
20 15 19 eqeltrid 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> dom ( F |` A ) e. dom vol )
21 resco 
 |-  ( ( Re o. F ) |` A ) = ( Re o. ( F |` A ) )
22 21 cnveqi 
 |-  `' ( ( Re o. F ) |` A ) = `' ( Re o. ( F |` A ) )
23 22 imaeq1i 
 |-  ( `' ( ( Re o. F ) |` A ) " ( x (,) +oo ) ) = ( `' ( Re o. ( F |` A ) ) " ( x (,) +oo ) )
24 cnvresima 
 |-  ( `' ( ( Re o. F ) |` A ) " ( x (,) +oo ) ) = ( ( `' ( Re o. F ) " ( x (,) +oo ) ) i^i A )
25 23 24 eqtr3i 
 |-  ( `' ( Re o. ( F |` A ) ) " ( x (,) +oo ) ) = ( ( `' ( Re o. F ) " ( x (,) +oo ) ) i^i A )
26 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
27 ismbfcn 
 |-  ( F : dom F --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
28 26 27 syl 
 |-  ( F e. MblFn -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
29 28 ibi 
 |-  ( F e. MblFn -> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) )
30 29 simpld 
 |-  ( F e. MblFn -> ( Re o. F ) e. MblFn )
31 fco 
 |-  ( ( Re : CC --> RR /\ F : dom F --> CC ) -> ( Re o. F ) : dom F --> RR )
32 1 26 31 sylancr 
 |-  ( F e. MblFn -> ( Re o. F ) : dom F --> RR )
33 mbfima 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Re o. F ) : dom F --> RR ) -> ( `' ( Re o. F ) " ( x (,) +oo ) ) e. dom vol )
34 30 32 33 syl2anc 
 |-  ( F e. MblFn -> ( `' ( Re o. F ) " ( x (,) +oo ) ) e. dom vol )
35 inmbl 
 |-  ( ( ( `' ( Re o. F ) " ( x (,) +oo ) ) e. dom vol /\ A e. dom vol ) -> ( ( `' ( Re o. F ) " ( x (,) +oo ) ) i^i A ) e. dom vol )
36 34 35 sylan 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( `' ( Re o. F ) " ( x (,) +oo ) ) i^i A ) e. dom vol )
37 25 36 eqeltrid 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( `' ( Re o. ( F |` A ) ) " ( x (,) +oo ) ) e. dom vol )
38 37 adantr 
 |-  ( ( ( F e. MblFn /\ A e. dom vol ) /\ x e. RR ) -> ( `' ( Re o. ( F |` A ) ) " ( x (,) +oo ) ) e. dom vol )
39 22 imaeq1i 
 |-  ( `' ( ( Re o. F ) |` A ) " ( -oo (,) x ) ) = ( `' ( Re o. ( F |` A ) ) " ( -oo (,) x ) )
40 cnvresima 
 |-  ( `' ( ( Re o. F ) |` A ) " ( -oo (,) x ) ) = ( ( `' ( Re o. F ) " ( -oo (,) x ) ) i^i A )
41 39 40 eqtr3i 
 |-  ( `' ( Re o. ( F |` A ) ) " ( -oo (,) x ) ) = ( ( `' ( Re o. F ) " ( -oo (,) x ) ) i^i A )
42 mbfima 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Re o. F ) : dom F --> RR ) -> ( `' ( Re o. F ) " ( -oo (,) x ) ) e. dom vol )
43 30 32 42 syl2anc 
 |-  ( F e. MblFn -> ( `' ( Re o. F ) " ( -oo (,) x ) ) e. dom vol )
44 inmbl 
 |-  ( ( ( `' ( Re o. F ) " ( -oo (,) x ) ) e. dom vol /\ A e. dom vol ) -> ( ( `' ( Re o. F ) " ( -oo (,) x ) ) i^i A ) e. dom vol )
45 43 44 sylan 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( `' ( Re o. F ) " ( -oo (,) x ) ) i^i A ) e. dom vol )
46 41 45 eqeltrid 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( `' ( Re o. ( F |` A ) ) " ( -oo (,) x ) ) e. dom vol )
47 46 adantr 
 |-  ( ( ( F e. MblFn /\ A e. dom vol ) /\ x e. RR ) -> ( `' ( Re o. ( F |` A ) ) " ( -oo (,) x ) ) e. dom vol )
48 14 20 38 47 ismbf2d 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( Re o. ( F |` A ) ) e. MblFn )
49 imf 
 |-  Im : CC --> RR
50 fco 
 |-  ( ( Im : CC --> RR /\ ( F |` A ) : dom ( F |` A ) --> CC ) -> ( Im o. ( F |` A ) ) : dom ( F |` A ) --> RR )
51 49 12 50 sylancr 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( Im o. ( F |` A ) ) : dom ( F |` A ) --> RR )
52 resco 
 |-  ( ( Im o. F ) |` A ) = ( Im o. ( F |` A ) )
53 52 cnveqi 
 |-  `' ( ( Im o. F ) |` A ) = `' ( Im o. ( F |` A ) )
54 53 imaeq1i 
 |-  ( `' ( ( Im o. F ) |` A ) " ( x (,) +oo ) ) = ( `' ( Im o. ( F |` A ) ) " ( x (,) +oo ) )
55 cnvresima 
 |-  ( `' ( ( Im o. F ) |` A ) " ( x (,) +oo ) ) = ( ( `' ( Im o. F ) " ( x (,) +oo ) ) i^i A )
56 54 55 eqtr3i 
 |-  ( `' ( Im o. ( F |` A ) ) " ( x (,) +oo ) ) = ( ( `' ( Im o. F ) " ( x (,) +oo ) ) i^i A )
57 29 simprd 
 |-  ( F e. MblFn -> ( Im o. F ) e. MblFn )
58 fco 
 |-  ( ( Im : CC --> RR /\ F : dom F --> CC ) -> ( Im o. F ) : dom F --> RR )
59 49 26 58 sylancr 
 |-  ( F e. MblFn -> ( Im o. F ) : dom F --> RR )
60 mbfima 
 |-  ( ( ( Im o. F ) e. MblFn /\ ( Im o. F ) : dom F --> RR ) -> ( `' ( Im o. F ) " ( x (,) +oo ) ) e. dom vol )
61 57 59 60 syl2anc 
 |-  ( F e. MblFn -> ( `' ( Im o. F ) " ( x (,) +oo ) ) e. dom vol )
62 inmbl 
 |-  ( ( ( `' ( Im o. F ) " ( x (,) +oo ) ) e. dom vol /\ A e. dom vol ) -> ( ( `' ( Im o. F ) " ( x (,) +oo ) ) i^i A ) e. dom vol )
63 61 62 sylan 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( `' ( Im o. F ) " ( x (,) +oo ) ) i^i A ) e. dom vol )
64 56 63 eqeltrid 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( `' ( Im o. ( F |` A ) ) " ( x (,) +oo ) ) e. dom vol )
65 64 adantr 
 |-  ( ( ( F e. MblFn /\ A e. dom vol ) /\ x e. RR ) -> ( `' ( Im o. ( F |` A ) ) " ( x (,) +oo ) ) e. dom vol )
66 53 imaeq1i 
 |-  ( `' ( ( Im o. F ) |` A ) " ( -oo (,) x ) ) = ( `' ( Im o. ( F |` A ) ) " ( -oo (,) x ) )
67 cnvresima 
 |-  ( `' ( ( Im o. F ) |` A ) " ( -oo (,) x ) ) = ( ( `' ( Im o. F ) " ( -oo (,) x ) ) i^i A )
68 66 67 eqtr3i 
 |-  ( `' ( Im o. ( F |` A ) ) " ( -oo (,) x ) ) = ( ( `' ( Im o. F ) " ( -oo (,) x ) ) i^i A )
69 mbfima 
 |-  ( ( ( Im o. F ) e. MblFn /\ ( Im o. F ) : dom F --> RR ) -> ( `' ( Im o. F ) " ( -oo (,) x ) ) e. dom vol )
70 57 59 69 syl2anc 
 |-  ( F e. MblFn -> ( `' ( Im o. F ) " ( -oo (,) x ) ) e. dom vol )
71 inmbl 
 |-  ( ( ( `' ( Im o. F ) " ( -oo (,) x ) ) e. dom vol /\ A e. dom vol ) -> ( ( `' ( Im o. F ) " ( -oo (,) x ) ) i^i A ) e. dom vol )
72 70 71 sylan 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( `' ( Im o. F ) " ( -oo (,) x ) ) i^i A ) e. dom vol )
73 68 72 eqeltrid 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( `' ( Im o. ( F |` A ) ) " ( -oo (,) x ) ) e. dom vol )
74 73 adantr 
 |-  ( ( ( F e. MblFn /\ A e. dom vol ) /\ x e. RR ) -> ( `' ( Im o. ( F |` A ) ) " ( -oo (,) x ) ) e. dom vol )
75 51 20 65 74 ismbf2d 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( Im o. ( F |` A ) ) e. MblFn )
76 ismbfcn 
 |-  ( ( F |` A ) : dom ( F |` A ) --> CC -> ( ( F |` A ) e. MblFn <-> ( ( Re o. ( F |` A ) ) e. MblFn /\ ( Im o. ( F |` A ) ) e. MblFn ) ) )
77 12 76 syl 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( ( F |` A ) e. MblFn <-> ( ( Re o. ( F |` A ) ) e. MblFn /\ ( Im o. ( F |` A ) ) e. MblFn ) ) )
78 48 75 77 mpbir2and 
 |-  ( ( F e. MblFn /\ A e. dom vol ) -> ( F |` A ) e. MblFn )