This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ismbfcn2

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

Ref Expression
Hypothesis ismbfcn2.1 
|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion ismbfcn2 
|- ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )

Proof

Step Hyp Ref Expression
1 ismbfcn2.1 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
2 1 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
3 ismbfcn 
 |-  ( ( x e. A |-> B ) : A --> CC -> ( ( x e. A |-> B ) e. MblFn <-> ( ( Re o. ( x e. A |-> B ) ) e. MblFn /\ ( Im o. ( x e. A |-> B ) ) e. MblFn ) ) )
4 2 3 syl 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( Re o. ( x e. A |-> B ) ) e. MblFn /\ ( Im o. ( x e. A |-> B ) ) e. MblFn ) ) )
5 ref 
 |-  Re : CC --> RR
6 5 a1i 
 |-  ( ph -> Re : CC --> RR )
7 6 1 cofmpt 
 |-  ( ph -> ( Re o. ( x e. A |-> B ) ) = ( x e. A |-> ( Re ` B ) ) )
8 7 eleq1d 
 |-  ( ph -> ( ( Re o. ( x e. A |-> B ) ) e. MblFn <-> ( x e. A |-> ( Re ` B ) ) e. MblFn ) )
9 imf 
 |-  Im : CC --> RR
10 9 a1i 
 |-  ( ph -> Im : CC --> RR )
11 10 1 cofmpt 
 |-  ( ph -> ( Im o. ( x e. A |-> B ) ) = ( x e. A |-> ( Im ` B ) ) )
12 11 eleq1d 
 |-  ( ph -> ( ( Im o. ( x e. A |-> B ) ) e. MblFn <-> ( x e. A |-> ( Im ` B ) ) e. MblFn ) )
13 8 12 anbi12d 
 |-  ( ph -> ( ( ( Re o. ( x e. A |-> B ) ) e. MblFn /\ ( Im o. ( x e. A |-> B ) ) e. MblFn ) <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )
14 4 13 bitrd 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )