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 ) ) )