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	$⊢ (φ \land x \in A) \to B \in ℂ$
	Assertion	ismbfcn2	$⊢ φ \to ((x \in A ⟼ B) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn))$

Proof

Step	Hyp	Ref	Expression
1		ismbfcn2.1	$⊢ (φ \land x \in A) \to B \in ℂ$
2	1	fmpttd	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℂ$
3		ismbfcn	$⊢ (x \in A ⟼ B) : A ⟶ ℂ \to ((x \in A ⟼ B) \in MblFn \leftrightarrow (ℜ \circ (x \in A ⟼ B) \in MblFn \land ℑ \circ (x \in A ⟼ B) \in MblFn))$
4	2 3	syl	$⊢ φ \to ((x \in A ⟼ B) \in MblFn \leftrightarrow (ℜ \circ (x \in A ⟼ B) \in MblFn \land ℑ \circ (x \in A ⟼ B) \in MblFn))$
5		ref	$⊢ ℜ : ℂ ⟶ ℝ$
6	5	a1i	$⊢ φ \to ℜ : ℂ ⟶ ℝ$
7	6 1	cofmpt	$⊢ φ \to ℜ \circ (x \in A ⟼ B) = (x \in A ⟼ ℜ (B))$
8	7	eleq1d	$⊢ φ \to (ℜ \circ (x \in A ⟼ B) \in MblFn \leftrightarrow (x \in A ⟼ ℜ (B)) \in MblFn)$
9		imf	$⊢ ℑ : ℂ ⟶ ℝ$
10	9	a1i	$⊢ φ \to ℑ : ℂ ⟶ ℝ$
11	10 1	cofmpt	$⊢ φ \to ℑ \circ (x \in A ⟼ B) = (x \in A ⟼ ℑ (B))$
12	11	eleq1d	$⊢ φ \to (ℑ \circ (x \in A ⟼ B) \in MblFn \leftrightarrow (x \in A ⟼ ℑ (B)) \in MblFn)$
13	8 12	anbi12d	$⊢ φ \to ((ℜ \circ (x \in A ⟼ B) \in MblFn \land ℑ \circ (x \in A ⟼ B) \in MblFn) \leftrightarrow ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn))$
14	4 13	bitrd	$⊢ φ \to ((x \in A ⟼ B) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn))$