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