ismbf

Description: The predicate " F is a measurable function". A function is measurable iff the preimages of all open intervals are measurable sets in the sense of ismbl . (Contributed by Mario Carneiro, 17-Jun-2014)

		Ref	Expression
	Assertion	ismbf	$⊢ F : A ⟶ ℝ \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol)$

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		ioomax	$⊢ (−∞, +∞) = ℝ$
6		ioorebas	$⊢ (−∞, +∞) \in ran (.)$
7	5 6	eqeltrri	$⊢ ℝ \in ran (.)$
8		imaeq2	$⊢ x = ℝ \to F^{-1} [x] = F^{-1} [ℝ]$
9	8	eleq1d	$⊢ x = ℝ \to (F^{-1} [x] \in dom vol \leftrightarrow F^{-1} [ℝ] \in dom vol)$
10	9	rspcv	$⊢ ℝ \in ran (.) \to (\forall x \in ran (.) F^{-1} [x] \in dom vol \to F^{-1} [ℝ] \in dom vol)$
11	7 10	ax-mp	$⊢ \forall x \in ran (.) F^{-1} [x] \in dom vol \to F^{-1} [ℝ] \in dom vol$
12		fimacnv	$⊢ F : A ⟶ ℝ \to F^{-1} [ℝ] = A$
13	12	eleq1d	$⊢ F : A ⟶ ℝ \to (F^{-1} [ℝ] \in dom vol \leftrightarrow A \in dom vol)$
14	11 13	imbitrid	$⊢ F : A ⟶ ℝ \to (\forall x \in ran (.) F^{-1} [x] \in dom vol \to A \in dom vol)$
15		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))$
16		ffvelcdm	$⊢ (F : A ⟶ ℝ \land x \in A) \to F (x) \in ℝ$
17	16	adantlr	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land x \in A) \to F (x) \in ℝ$
18	17	rered	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land x \in A) \to ℜ (F (x)) = F (x)$
19	18	mpteq2dva	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (x \in A ⟼ ℜ (F (x))) = (x \in A ⟼ F (x))$
20	17	recnd	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land x \in A) \to F (x) \in ℂ$
21		simpl	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F : A ⟶ ℝ$
22	21	feqmptd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F = (x \in A ⟼ F (x))$
23		ref	$⊢ ℜ : ℂ ⟶ ℝ$
24	23	a1i	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℜ : ℂ ⟶ ℝ$
25	24	feqmptd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℜ = (y \in ℂ ⟼ ℜ (y))$
26		fveq2	$⊢ y = F (x) \to ℜ (y) = ℜ (F (x))$
27	20 22 25 26	fmptco	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℜ \circ F = (x \in A ⟼ ℜ (F (x)))$
28	19 27 22	3eqtr4rd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F = ℜ \circ F$
29	28	cnveqd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F^{-1} = {(ℜ \circ F)}^{-1}$
30	29	imaeq1d	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F^{-1} [x] = {(ℜ \circ F)}^{-1} [x]$
31	30	eleq1d	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (F^{-1} [x] \in dom vol \leftrightarrow {(ℜ \circ F)}^{-1} [x] \in dom vol)$
32		imf	$⊢ ℑ : ℂ ⟶ ℝ$
33	32	a1i	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℑ : ℂ ⟶ ℝ$
34	33	feqmptd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℑ = (y \in ℂ ⟼ ℑ (y))$
35		fveq2	$⊢ y = F (x) \to ℑ (y) = ℑ (F (x))$
36	20 22 34 35	fmptco	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℑ \circ F = (x \in A ⟼ ℑ (F (x)))$
37	17	reim0d	$⊢ ((F : A ⟶ ℝ \land A \in dom vol) \land x \in A) \to ℑ (F (x)) = 0$
38	37	mpteq2dva	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (x \in A ⟼ ℑ (F (x))) = (x \in A ⟼ 0)$
39	36 38	eqtrd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℑ \circ F = (x \in A ⟼ 0)$
40		fconstmpt	$⊢ A \times \{0\} = (x \in A ⟼ 0)$
41	39 40	eqtr4di	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ℑ \circ F = A \times \{0\}$
42	41	cnveqd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to {(ℑ \circ F)}^{-1} = {(A \times \{0\})}^{-1}$
43	42	imaeq1d	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to {(ℑ \circ F)}^{-1} [x] = {(A \times \{0\})}^{-1} [x]$
44		simpr	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to A \in dom vol$
45		0re	$⊢ 0 \in ℝ$
46		mbfconstlem	$⊢ (A \in dom vol \land 0 \in ℝ) \to {(A \times \{0\})}^{-1} [x] \in dom vol$
47	44 45 46	sylancl	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to {(A \times \{0\})}^{-1} [x] \in dom vol$
48	43 47	eqeltrd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to {(ℑ \circ F)}^{-1} [x] \in dom vol$
49	48	biantrud	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to ({(ℜ \circ F)}^{-1} [x] \in dom vol \leftrightarrow ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
50	31 49	bitrd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (F^{-1} [x] \in dom vol \leftrightarrow ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
51	50	ralbidv	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (\forall x \in ran (.) F^{-1} [x] \in dom vol \leftrightarrow \forall x \in ran (.) ({(ℜ \circ F)}^{-1} [x] \in dom vol \land {(ℑ \circ F)}^{-1} [x] \in dom vol))$
52		ax-resscn	$⊢ ℝ \subseteq ℂ$
53		fss	$⊢ (F : A ⟶ ℝ \land ℝ \subseteq ℂ) \to F : A ⟶ ℂ$
54	52 53	mpan2	$⊢ F : A ⟶ ℝ \to F : A ⟶ ℂ$
55		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
56		cnex	$⊢ ℂ \in V$
57		reex	$⊢ ℝ \in V$
58		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℝ)) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
59	56 57 58	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℝ) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
60	54 55 59	syl2an	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
61	60	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)))$
62	51 61	bitrd	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (\forall x \in ran (.) 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)))$
63	15 62	bitr4id	$⊢ (F : A ⟶ ℝ \land A \in dom vol) \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol)$
64	63	ex	$⊢ F : A ⟶ ℝ \to (A \in dom vol \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol))$
65	4 14 64	pm5.21ndd	$⊢ F : A ⟶ ℝ \to (F \in MblFn \leftrightarrow \forall x \in ran (.) F^{-1} [x] \in dom vol)$

Metamath Proof Explorer

Theorem ismbf

Proof