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 ⊢ φ ∧ x ∈ A → B ∈ ℂ
Assertion ismbfcn2 ⊢ φ → x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn

Proof

Step Hyp Ref Expression
1 ismbfcn2.1 ⊢ φ ∧ x ∈ A → B ∈ ℂ
2 1 fmpttd ⊢ φ → x ∈ A ⟼ B : A ⟶ ℂ
3 ismbfcn ⊢ x ∈ A ⟼ B : A ⟶ ℂ → x ∈ A ⟼ B ∈ MblFn ↔ ℜ ∘ x ∈ A ⟼ B ∈ MblFn ∧ ℑ ∘ x ∈ A ⟼ B ∈ MblFn
4 2 3 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn ↔ ℜ ∘ x ∈ A ⟼ B ∈ MblFn ∧ ℑ ∘ x ∈ A ⟼ B ∈ MblFn
5 ref ⊢ ℜ : ℂ ⟶ ℝ
6 5 a1i ⊢ φ → ℜ : ℂ ⟶ ℝ
7 6 1 cofmpt ⊢ φ → ℜ ∘ x ∈ A ⟼ B = x ∈ A ⟼ ℜ ⁡ B
8 7 eleq1d ⊢ φ → ℜ ∘ x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn
9 imf ⊢ ℑ : ℂ ⟶ ℝ
10 9 a1i ⊢ φ → ℑ : ℂ ⟶ ℝ
11 10 1 cofmpt ⊢ φ → ℑ ∘ x ∈ A ⟼ B = x ∈ A ⟼ ℑ ⁡ B
12 11 eleq1d ⊢ φ → ℑ ∘ x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn
13 8 12 anbi12d ⊢ φ → ℜ ∘ x ∈ A ⟼ B ∈ MblFn ∧ ℑ ∘ x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn
14 4 13 bitrd ⊢ φ → x ∈ A ⟼ B ∈ MblFn ↔ x ∈ A ⟼ ℜ ⁡ B ∈ MblFn ∧ x ∈ A ⟼ ℑ ⁡ B ∈ MblFn