mbfres

Description: The restriction of a measurable function is measurable. (Contributed by Mario Carneiro, 18-Jun-2014)

		Ref	Expression
	Assertion	mbfres	$⊢ (F \in MblFn \land A \in dom vol) \to {F ↾}_{A} \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		ref	$⊢ ℜ : ℂ ⟶ ℝ$
2		simpr	$⊢ (F \in MblFn \land A \in dom vol) \to A \in dom vol$
3		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))$
4	3	simplbi	$⊢ F \in MblFn \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
5	4	adantr	$⊢ (F \in MblFn \land A \in dom vol) \to F \in (ℂ ↑_{𝑝𝑚} ℝ)$
6		pmresg	$⊢ (A \in dom vol \land F \in (ℂ ↑_{𝑝𝑚} ℝ)) \to {F ↾}_{A} \in (ℂ ↑_{𝑝𝑚} A)$
7	2 5 6	syl2anc	$⊢ (F \in MblFn \land A \in dom vol) \to {F ↾}_{A} \in (ℂ ↑_{𝑝𝑚} A)$
8		cnex	$⊢ ℂ \in V$
9		elpm2g	$⊢ (ℂ \in V \land A \in dom vol) \to ({F ↾}_{A} \in (ℂ ↑_{𝑝𝑚} A) \leftrightarrow (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \land dom ({F ↾}_{A}) \subseteq A))$
10	8 2 9	sylancr	$⊢ (F \in MblFn \land A \in dom vol) \to ({F ↾}_{A} \in (ℂ ↑_{𝑝𝑚} A) \leftrightarrow (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \land dom ({F ↾}_{A}) \subseteq A))$
11	7 10	mpbid	$⊢ (F \in MblFn \land A \in dom vol) \to (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \land dom ({F ↾}_{A}) \subseteq A)$
12	11	simpld	$⊢ (F \in MblFn \land A \in dom vol) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ$
13		fco	$⊢ (ℜ : ℂ ⟶ ℝ \land ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ) \to (ℜ \circ ({F ↾}_{A})) : dom ({F ↾}_{A}) ⟶ ℝ$
14	1 12 13	sylancr	$⊢ (F \in MblFn \land A \in dom vol) \to (ℜ \circ ({F ↾}_{A})) : dom ({F ↾}_{A}) ⟶ ℝ$
15		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
16		id	$⊢ A \in dom vol \to A \in dom vol$
17		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
18		inmbl	$⊢ (A \in dom vol \land dom F \in dom vol) \to A \cap dom F \in dom vol$
19	16 17 18	syl2anr	$⊢ (F \in MblFn \land A \in dom vol) \to A \cap dom F \in dom vol$
20	15 19	eqeltrid	$⊢ (F \in MblFn \land A \in dom vol) \to dom ({F ↾}_{A}) \in dom vol$
21		resco	$⊢ {(ℜ \circ F) ↾}_{A} = ℜ \circ ({F ↾}_{A})$
22	21	cnveqi	$⊢ {({(ℜ \circ F) ↾}_{A})}^{-1} = {(ℜ \circ ({F ↾}_{A}))}^{-1}$
23	22	imaeq1i	$⊢ {({(ℜ \circ F) ↾}_{A})}^{-1} [(x, +∞)] = {(ℜ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)]$
24		cnvresima	$⊢ {({(ℜ \circ F) ↾}_{A})}^{-1} [(x, +∞)] = {(ℜ \circ F)}^{-1} [(x, +∞)] \cap A$
25	23 24	eqtr3i	$⊢ {(ℜ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)] = {(ℜ \circ F)}^{-1} [(x, +∞)] \cap A$
26		mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$
27		ismbfcn	$⊢ F : dom F ⟶ ℂ \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$
28	26 27	syl	$⊢ F \in MblFn \to (F \in MblFn \leftrightarrow (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn))$
29	28	ibi	$⊢ F \in MblFn \to (ℜ \circ F \in MblFn \land ℑ \circ F \in MblFn)$
30	29	simpld	$⊢ F \in MblFn \to ℜ \circ F \in MblFn$
31		fco	$⊢ (ℜ : ℂ ⟶ ℝ \land F : dom F ⟶ ℂ) \to (ℜ \circ F) : dom F ⟶ ℝ$
32	1 26 31	sylancr	$⊢ F \in MblFn \to (ℜ \circ F) : dom F ⟶ ℝ$
33		mbfima	$⊢ (ℜ \circ F \in MblFn \land (ℜ \circ F) : dom F ⟶ ℝ) \to {(ℜ \circ F)}^{-1} [(x, +∞)] \in dom vol$
34	30 32 33	syl2anc	$⊢ F \in MblFn \to {(ℜ \circ F)}^{-1} [(x, +∞)] \in dom vol$
35		inmbl	$⊢ ({(ℜ \circ F)}^{-1} [(x, +∞)] \in dom vol \land A \in dom vol) \to {(ℜ \circ F)}^{-1} [(x, +∞)] \cap A \in dom vol$
36	34 35	sylan	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℜ \circ F)}^{-1} [(x, +∞)] \cap A \in dom vol$
37	25 36	eqeltrid	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℜ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)] \in dom vol$
38	37	adantr	$⊢ ((F \in MblFn \land A \in dom vol) \land x \in ℝ) \to {(ℜ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)] \in dom vol$
39	22	imaeq1i	$⊢ {({(ℜ \circ F) ↾}_{A})}^{-1} [(−∞, x)] = {(ℜ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)]$
40		cnvresima	$⊢ {({(ℜ \circ F) ↾}_{A})}^{-1} [(−∞, x)] = {(ℜ \circ F)}^{-1} [(−∞, x)] \cap A$
41	39 40	eqtr3i	$⊢ {(ℜ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)] = {(ℜ \circ F)}^{-1} [(−∞, x)] \cap A$
42		mbfima	$⊢ (ℜ \circ F \in MblFn \land (ℜ \circ F) : dom F ⟶ ℝ) \to {(ℜ \circ F)}^{-1} [(−∞, x)] \in dom vol$
43	30 32 42	syl2anc	$⊢ F \in MblFn \to {(ℜ \circ F)}^{-1} [(−∞, x)] \in dom vol$
44		inmbl	$⊢ ({(ℜ \circ F)}^{-1} [(−∞, x)] \in dom vol \land A \in dom vol) \to {(ℜ \circ F)}^{-1} [(−∞, x)] \cap A \in dom vol$
45	43 44	sylan	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℜ \circ F)}^{-1} [(−∞, x)] \cap A \in dom vol$
46	41 45	eqeltrid	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℜ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)] \in dom vol$
47	46	adantr	$⊢ ((F \in MblFn \land A \in dom vol) \land x \in ℝ) \to {(ℜ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)] \in dom vol$
48	14 20 38 47	ismbf2d	$⊢ (F \in MblFn \land A \in dom vol) \to ℜ \circ ({F ↾}_{A}) \in MblFn$
49		imf	$⊢ ℑ : ℂ ⟶ ℝ$
50		fco	$⊢ (ℑ : ℂ ⟶ ℝ \land ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ) \to (ℑ \circ ({F ↾}_{A})) : dom ({F ↾}_{A}) ⟶ ℝ$
51	49 12 50	sylancr	$⊢ (F \in MblFn \land A \in dom vol) \to (ℑ \circ ({F ↾}_{A})) : dom ({F ↾}_{A}) ⟶ ℝ$
52		resco	$⊢ {(ℑ \circ F) ↾}_{A} = ℑ \circ ({F ↾}_{A})$
53	52	cnveqi	$⊢ {({(ℑ \circ F) ↾}_{A})}^{-1} = {(ℑ \circ ({F ↾}_{A}))}^{-1}$
54	53	imaeq1i	$⊢ {({(ℑ \circ F) ↾}_{A})}^{-1} [(x, +∞)] = {(ℑ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)]$
55		cnvresima	$⊢ {({(ℑ \circ F) ↾}_{A})}^{-1} [(x, +∞)] = {(ℑ \circ F)}^{-1} [(x, +∞)] \cap A$
56	54 55	eqtr3i	$⊢ {(ℑ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)] = {(ℑ \circ F)}^{-1} [(x, +∞)] \cap A$
57	29	simprd	$⊢ F \in MblFn \to ℑ \circ F \in MblFn$
58		fco	$⊢ (ℑ : ℂ ⟶ ℝ \land F : dom F ⟶ ℂ) \to (ℑ \circ F) : dom F ⟶ ℝ$
59	49 26 58	sylancr	$⊢ F \in MblFn \to (ℑ \circ F) : dom F ⟶ ℝ$
60		mbfima	$⊢ (ℑ \circ F \in MblFn \land (ℑ \circ F) : dom F ⟶ ℝ) \to {(ℑ \circ F)}^{-1} [(x, +∞)] \in dom vol$
61	57 59 60	syl2anc	$⊢ F \in MblFn \to {(ℑ \circ F)}^{-1} [(x, +∞)] \in dom vol$
62		inmbl	$⊢ ({(ℑ \circ F)}^{-1} [(x, +∞)] \in dom vol \land A \in dom vol) \to {(ℑ \circ F)}^{-1} [(x, +∞)] \cap A \in dom vol$
63	61 62	sylan	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℑ \circ F)}^{-1} [(x, +∞)] \cap A \in dom vol$
64	56 63	eqeltrid	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℑ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)] \in dom vol$
65	64	adantr	$⊢ ((F \in MblFn \land A \in dom vol) \land x \in ℝ) \to {(ℑ \circ ({F ↾}_{A}))}^{-1} [(x, +∞)] \in dom vol$
66	53	imaeq1i	$⊢ {({(ℑ \circ F) ↾}_{A})}^{-1} [(−∞, x)] = {(ℑ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)]$
67		cnvresima	$⊢ {({(ℑ \circ F) ↾}_{A})}^{-1} [(−∞, x)] = {(ℑ \circ F)}^{-1} [(−∞, x)] \cap A$
68	66 67	eqtr3i	$⊢ {(ℑ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)] = {(ℑ \circ F)}^{-1} [(−∞, x)] \cap A$
69		mbfima	$⊢ (ℑ \circ F \in MblFn \land (ℑ \circ F) : dom F ⟶ ℝ) \to {(ℑ \circ F)}^{-1} [(−∞, x)] \in dom vol$
70	57 59 69	syl2anc	$⊢ F \in MblFn \to {(ℑ \circ F)}^{-1} [(−∞, x)] \in dom vol$
71		inmbl	$⊢ ({(ℑ \circ F)}^{-1} [(−∞, x)] \in dom vol \land A \in dom vol) \to {(ℑ \circ F)}^{-1} [(−∞, x)] \cap A \in dom vol$
72	70 71	sylan	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℑ \circ F)}^{-1} [(−∞, x)] \cap A \in dom vol$
73	68 72	eqeltrid	$⊢ (F \in MblFn \land A \in dom vol) \to {(ℑ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)] \in dom vol$
74	73	adantr	$⊢ ((F \in MblFn \land A \in dom vol) \land x \in ℝ) \to {(ℑ \circ ({F ↾}_{A}))}^{-1} [(−∞, x)] \in dom vol$
75	51 20 65 74	ismbf2d	$⊢ (F \in MblFn \land A \in dom vol) \to ℑ \circ ({F ↾}_{A}) \in MblFn$
76		ismbfcn	$⊢ ({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \to ({F ↾}_{A} \in MblFn \leftrightarrow (ℜ \circ ({F ↾}_{A}) \in MblFn \land ℑ \circ ({F ↾}_{A}) \in MblFn))$
77	12 76	syl	$⊢ (F \in MblFn \land A \in dom vol) \to ({F ↾}_{A} \in MblFn \leftrightarrow (ℜ \circ ({F ↾}_{A}) \in MblFn \land ℑ \circ ({F ↾}_{A}) \in MblFn))$
78	48 75 77	mpbir2and	$⊢ (F \in MblFn \land A \in dom vol) \to {F ↾}_{A} \in MblFn$

Metamath Proof Explorer

Theorem mbfres

Proof