Metamath Proof Explorer

Theorem ismbfcn

Description: A complex function is measurable iff the real and imaginary components of the function are measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion ismbfcn 
|- ( F : A --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )

Proof

Step Hyp Ref Expression
1 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
2 fdm 
 |-  ( F : A --> CC -> dom F = A )
3 2 eleq1d 
 |-  ( F : A --> CC -> ( dom F e. dom vol <-> A e. dom vol ) )
4 1 3 imbitrid 
 |-  ( F : A --> CC -> ( F e. MblFn -> A e. dom vol ) )
5 mbfdm 
 |-  ( ( Re o. F ) e. MblFn -> dom ( Re o. F ) e. dom vol )
6 5 adantr 
 |-  ( ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) -> dom ( Re o. F ) e. dom vol )
7 ref 
 |-  Re : CC --> RR
8 fco 
 |-  ( ( Re : CC --> RR /\ F : A --> CC ) -> ( Re o. F ) : A --> RR )
9 7 8 mpan 
 |-  ( F : A --> CC -> ( Re o. F ) : A --> RR )
10 9 fdmd 
 |-  ( F : A --> CC -> dom ( Re o. F ) = A )
11 10 eleq1d 
 |-  ( F : A --> CC -> ( dom ( Re o. F ) e. dom vol <-> A e. dom vol ) )
12 6 11 imbitrid 
 |-  ( F : A --> CC -> ( ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) -> A e. dom vol ) )
13 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 ) ) )
14 9 adantr 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( Re o. F ) : A --> RR )
15 ismbf 
 |-  ( ( Re o. F ) : A --> RR -> ( ( Re o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) )
16 14 15 syl 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( ( Re o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol ) )
17 imf 
 |-  Im : CC --> RR
18 fco 
 |-  ( ( Im : CC --> RR /\ F : A --> CC ) -> ( Im o. F ) : A --> RR )
19 17 18 mpan 
 |-  ( F : A --> CC -> ( Im o. F ) : A --> RR )
20 19 adantr 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( Im o. F ) : A --> RR )
21 ismbf 
 |-  ( ( Im o. F ) : A --> RR -> ( ( Im o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Im o. F ) " x ) e. dom vol ) )
22 20 21 syl 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( ( Im o. F ) e. MblFn <-> A. x e. ran (,) ( `' ( Im o. F ) " x ) e. dom vol ) )
23 16 22 anbi12d 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) <-> ( A. x e. ran (,) ( `' ( Re o. F ) " x ) e. dom vol /\ A. x e. ran (,) ( `' ( Im o. F ) " x ) e. dom vol ) ) )
24 r19.26 
 |-  ( 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 /\ A. x e. ran (,) ( `' ( Im o. F ) " x ) e. dom vol ) )
25 23 24 bitr4di 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) <-> A. x e. ran (,) ( ( `' ( Re o. F ) " x ) e. dom vol /\ ( `' ( Im o. F ) " x ) e. dom vol ) ) )
26 mblss 
 |-  ( A e. dom vol -> A C_ RR )
27 cnex 
 |-  CC e. _V
28 reex 
 |-  RR e. _V
29 elpm2r 
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
30 27 28 29 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) )
31 26 30 sylan2 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> F e. ( CC ^pm RR ) )
32 31 biantrurd 
 |-  ( ( F : A --> CC /\ 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 ) ) ) )
33 25 32 bitrd 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( ( ( Re o. F ) e. MblFn /\ ( Im o. 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 ) ) ) )
34 13 33 bitr4id 
 |-  ( ( F : A --> CC /\ A e. dom vol ) -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
35 34 ex 
 |-  ( F : A --> CC -> ( A e. dom vol -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) ) )
36 4 12 35 pm5.21ndd 
 |-  ( F : A --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )