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 ( 𝐹 : 𝐴 ⟶ ℂ → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )

Proof

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