This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion ismbfcn2 ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )

Proof

Step Hyp Ref Expression
1 ismbfcn2.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
2 1 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
3 ismbfcn ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ) ) )
4 2 3 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ) ) )
5 ref ⊢ ℜ : ℂ ⟶ ℝ
6 5 a1i ⊢ ( 𝜑 → ℜ : ℂ ⟶ ℝ )
7 6 1 cofmpt ⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) )
8 7 eleq1d ⊢ ( 𝜑 → ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ) )
9 imf ⊢ ℑ : ℂ ⟶ ℝ
10 9 a1i ⊢ ( 𝜑 → ℑ : ℂ ⟶ ℝ )
11 10 1 cofmpt ⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) )
12 11 eleq1d ⊢ ( 𝜑 → ( ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) )
13 8 12 anbi12d ⊢ ( 𝜑 → ( ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
14 4 13 bitrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )