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	$⊢ F : A ⟶ ℂ \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$

Proof

Step	Hyp	Ref	Expression
1		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
2		fdm	$⊢ F : A ⟶ ℂ \to dom F = A$
3	2	eleq1d	$⊢ F : A ⟶ ℂ \to (dom F \in dom vol \leftrightarrow A \in dom vol)$
4	1 3	imbitrid	$⊢ F : A ⟶ ℂ \to (F \in MblFn \to A \in dom vol)$
5		mbfdm	$⊢ ℜ \circ F \in MblFn \to dom (ℜ \circ F) \in dom vol$
6	5	adantr	$⊢ (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn) \to dom (ℜ \circ F) \in dom vol$
7		ref	$⊢ ℜ : ℂ ⟶ ℝ$
8		fco	$⊢ (ℜ : ℂ ⟶ ℝ \land F : A ⟶ ℂ) \to (ℜ \circ F) : A ⟶ ℝ$
9	7 8	mpan	$⊢ F : A ⟶ ℂ \to (ℜ \circ F) : A ⟶ ℝ$
10	9	fdmd	$⊢ F : A ⟶ ℂ \to dom (ℜ \circ F) = A$
11	10	eleq1d	$⊢ F : A ⟶ ℂ \to (dom (ℜ \circ F) \in dom vol \leftrightarrow A \in dom vol)$
12	6 11	imbitrid	$⊢ F : A ⟶ ℂ \to ((ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn) \to A \in dom vol)$
13		ismbf1	$⊢ F \in MblFn \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
14	9	adantr	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to (ℜ \circ F) : A ⟶ ℝ$
15		ismbf	$⊢ (ℜ \circ F) : A ⟶ ℝ \to (ℜ \circ F \in MblFn \leftrightarrow \forall x \in ran (.) {(ℜ \circ F)}^{-1} [x] \in dom vol)$
16	14 15	syl	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to (ℜ \circ F \in MblFn \leftrightarrow \forall x \in ran (.) {(ℜ \circ F)}^{-1} [x] \in dom vol)$
17		imf	$⊢ ℑ : ℂ ⟶ ℝ$
18		fco	$⊢ (ℑ : ℂ ⟶ ℝ \land F : A ⟶ ℂ) \to (ℑ \circ F) : A ⟶ ℝ$
19	17 18	mpan	$⊢ F : A ⟶ ℂ \to (ℑ \circ F) : A ⟶ ℝ$
20	19	adantr	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to (ℑ \circ F) : A ⟶ ℝ$
21		ismbf	$⊢ (ℑ \circ F) : A ⟶ ℝ \to (ℑ \circ F \in MblFn \leftrightarrow \forall x \in ran (.) {(ℑ \circ F)}^{-1} [x] \in dom vol)$
22	20 21	syl	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to (ℑ \circ F \in MblFn \leftrightarrow \forall x \in ran (.) {(ℑ \circ F)}^{-1} [x] \in dom vol)$
23	16 22	anbi12d	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to ((ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn) \leftrightarrow (\forall x \in ran (.) {(ℜ \circ F)}^{-1} [x] \in dom vol \land \forall x \in ran (.) {(ℑ \circ F)}^{-1} [x] \in dom vol))$
24		r19.26	$⊢ \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol) \leftrightarrow (\forall x \in ran (.) {(ℜ \circ F)}^{-1} [x] \in dom vol \land \forall x \in ran (.) {(ℑ \circ F)}^{-1} [x] \in dom vol)$
25	23 24	bitr4di	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to ((ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn) \leftrightarrow \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
26		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
27		cnex	$⊢ ℂ \in V$
28		reex	$⊢ ℝ \in V$
29		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
30	27 28 29	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
31	26 30	sylan2	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
32	31	biantrurd	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to (\forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol)))$
33	25 32	bitrd	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to ((ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol)))$
34	13 33	bitr4id	$⊢ (F : A ⟶ ℂ \land A \in dom vol) \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$
35	34	ex	$⊢ F : A ⟶ ℂ \to (A \in dom vol \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn)))$
36	4 12 35	pm5.21ndd	$⊢ F : A ⟶ ℂ \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$

Metamath Proof Explorer

Theorem ismbfcn

Proof