# 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 ⟶ ℂ → F ∈ MblFn ↔ ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn$

### Proof

Step Hyp Ref Expression
1 mbfdm $⊢ F ∈ MblFn → dom ⁡ F ∈ dom ⁡ vol$
2 fdm $⊢ F : A ⟶ ℂ → dom ⁡ F = A$
3 2 eleq1d $⊢ F : A ⟶ ℂ → dom ⁡ F ∈ dom ⁡ vol ↔ A ∈ dom ⁡ vol$
4 1 3 syl5ib $⊢ F : A ⟶ ℂ → F ∈ MblFn → A ∈ dom ⁡ vol$
5 mbfdm $⊢ ℜ ∘ F ∈ MblFn → dom ⁡ ℜ ∘ F ∈ dom ⁡ vol$
6 5 adantr $⊢ ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn → dom ⁡ ℜ ∘ F ∈ dom ⁡ vol$
7 ref $⊢ ℜ : ℂ ⟶ ℝ$
8 fco $⊢ ℜ : ℂ ⟶ ℝ ∧ F : A ⟶ ℂ → ℜ ∘ F : A ⟶ ℝ$
9 7 8 mpan $⊢ F : A ⟶ ℂ → ℜ ∘ F : A ⟶ ℝ$
10 9 fdmd $⊢ F : A ⟶ ℂ → dom ⁡ ℜ ∘ F = A$
11 10 eleq1d $⊢ F : A ⟶ ℂ → dom ⁡ ℜ ∘ F ∈ dom ⁡ vol ↔ A ∈ dom ⁡ vol$
12 6 11 syl5ib $⊢ F : A ⟶ ℂ → ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn → A ∈ dom ⁡ vol$
13 ismbf1 $⊢ F ∈ MblFn ↔ F ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol$
14 9 adantr $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℜ ∘ F : A ⟶ ℝ$
15 ismbf $⊢ ℜ ∘ F : A ⟶ ℝ → ℜ ∘ F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol$
16 14 15 syl $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℜ ∘ F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol$
17 imf $⊢ ℑ : ℂ ⟶ ℝ$
18 fco $⊢ ℑ : ℂ ⟶ ℝ ∧ F : A ⟶ ℂ → ℑ ∘ F : A ⟶ ℝ$
19 17 18 mpan $⊢ F : A ⟶ ℂ → ℑ ∘ F : A ⟶ ℝ$
20 19 adantr $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℑ ∘ F : A ⟶ ℝ$
21 ismbf $⊢ ℑ ∘ F : A ⟶ ℝ → ℑ ∘ F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . ℑ ∘ F -1 x ∈ dom ⁡ vol$
22 20 21 syl $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℑ ∘ F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . ℑ ∘ F -1 x ∈ dom ⁡ vol$
23 16 22 anbi12d $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ∀ x ∈ ran ⁡ . ℑ ∘ F -1 x ∈ dom ⁡ vol$
24 r19.26 $⊢ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol ↔ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ∀ x ∈ ran ⁡ . ℑ ∘ F -1 x ∈ dom ⁡ vol$
25 23 24 bitr4di $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn ↔ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol$
26 mblss $⊢ A ∈ dom ⁡ vol → A ⊆ ℝ$
27 cnex $⊢ ℂ ∈ V$
28 reex $⊢ ℝ ∈ V$
29 elpm2r $⊢ ℂ ∈ V ∧ ℝ ∈ V ∧ F : A ⟶ ℂ ∧ A ⊆ ℝ → F ∈ ℂ ↑ 𝑝𝑚 ℝ$
30 27 28 29 mpanl12 $⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → F ∈ ℂ ↑ 𝑝𝑚 ℝ$
31 26 30 sylan2 $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → F ∈ ℂ ↑ 𝑝𝑚 ℝ$
32 31 biantrurd $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol ↔ F ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol$
33 25 32 bitrd $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn ↔ F ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol$
34 13 33 bitr4id $⊢ F : A ⟶ ℂ ∧ A ∈ dom ⁡ vol → F ∈ MblFn ↔ ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn$
35 34 ex $⊢ F : A ⟶ ℂ → A ∈ dom ⁡ vol → F ∈ MblFn ↔ ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn$
36 4 12 35 pm5.21ndd $⊢ F : A ⟶ ℂ → F ∈ MblFn ↔ ℜ ∘ F ∈ MblFn ∧ ℑ ∘ F ∈ MblFn$