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