# 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 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
Assertion ismbfcn2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in MblFn↔\left(\left({x}\in {A}⟼\Re \left({B}\right)\right)\in MblFn\wedge \left({x}\in {A}⟼\Im \left({B}\right)\right)\in MblFn\right)\right)$

### Proof

Step Hyp Ref Expression
1 ismbfcn2.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
2 1 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶ℂ$
3 ismbfcn ${⊢}\left({x}\in {A}⟼{B}\right):{A}⟶ℂ\to \left(\left({x}\in {A}⟼{B}\right)\in MblFn↔\left(\Re \circ \left({x}\in {A}⟼{B}\right)\in MblFn\wedge \Im \circ \left({x}\in {A}⟼{B}\right)\in MblFn\right)\right)$
4 2 3 syl ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in MblFn↔\left(\Re \circ \left({x}\in {A}⟼{B}\right)\in MblFn\wedge \Im \circ \left({x}\in {A}⟼{B}\right)\in MblFn\right)\right)$
5 ref ${⊢}\Re :ℂ⟶ℝ$
6 5 a1i ${⊢}{\phi }\to \Re :ℂ⟶ℝ$
7 6 1 cofmpt ${⊢}{\phi }\to \Re \circ \left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼\Re \left({B}\right)\right)$
8 7 eleq1d ${⊢}{\phi }\to \left(\Re \circ \left({x}\in {A}⟼{B}\right)\in MblFn↔\left({x}\in {A}⟼\Re \left({B}\right)\right)\in MblFn\right)$
9 imf ${⊢}\Im :ℂ⟶ℝ$
10 9 a1i ${⊢}{\phi }\to \Im :ℂ⟶ℝ$
11 10 1 cofmpt ${⊢}{\phi }\to \Im \circ \left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼\Im \left({B}\right)\right)$
12 11 eleq1d ${⊢}{\phi }\to \left(\Im \circ \left({x}\in {A}⟼{B}\right)\in MblFn↔\left({x}\in {A}⟼\Im \left({B}\right)\right)\in MblFn\right)$
13 8 12 anbi12d ${⊢}{\phi }\to \left(\left(\Re \circ \left({x}\in {A}⟼{B}\right)\in MblFn\wedge \Im \circ \left({x}\in {A}⟼{B}\right)\in MblFn\right)↔\left(\left({x}\in {A}⟼\Re \left({B}\right)\right)\in MblFn\wedge \left({x}\in {A}⟼\Im \left({B}\right)\right)\in MblFn\right)\right)$
14 4 13 bitrd ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in MblFn↔\left(\left({x}\in {A}⟼\Re \left({B}\right)\right)\in MblFn\wedge \left({x}\in {A}⟼\Im \left({B}\right)\right)\in MblFn\right)\right)$