Metamath Proof Explorer

Theorem mbfres

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

Ref Expression
Assertion mbfres ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( 𝐹 ↾ 𝐴 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 ref ⊢ ℜ : ℂ ⟶ ℝ
2 simpr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → 𝐴 ∈ dom vol )
3 ismbf1 ⊢ ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
4 3 simplbi ⊢ ( 𝐹 ∈ MblFn → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
5 4 adantr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
6 pmresg ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐹 ∈ ( ℂ ↑pm ℝ ) ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ℂ ↑pm 𝐴 ) )
7 2 5 6 syl2anc ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( 𝐹 ↾ 𝐴 ) ∈ ( ℂ ↑pm 𝐴 ) )
8 cnex ⊢ ℂ ∈ V
9 elpm2g ⊢ ( ( ℂ ∈ V ∧ 𝐴 ∈ dom vol ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ℂ ↑pm 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ ∧ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ) ) )
10 8 2 9 sylancr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( 𝐹 ↾ 𝐴 ) ∈ ( ℂ ↑pm 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ ∧ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ) ) )
11 7 10 mpbid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ ∧ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ) )
12 11 simpld ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ )
13 fco ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ ) → ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℝ )
14 1 12 13 sylancr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℝ )
15 dmres ⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
16 id ⊢ ( 𝐴 ∈ dom vol → 𝐴 ∈ dom vol )
17 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
18 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ dom 𝐹 ∈ dom vol ) → ( 𝐴 ∩ dom 𝐹 ) ∈ dom vol )
19 16 17 18 syl2anr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( 𝐴 ∩ dom 𝐹 ) ∈ dom vol )
20 15 19 eqeltrid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → dom ( 𝐹 ↾ 𝐴 ) ∈ dom vol )
21 resco ⊢ ( ( ℜ ∘ 𝐹 ) ↾ 𝐴 ) = ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) )
22 21 cnveqi ⊢ ◡ ( ( ℜ ∘ 𝐹 ) ↾ 𝐴 ) = ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) )
23 22 imaeq1i ⊢ ( ◡ ( ( ℜ ∘ 𝐹 ) ↾ 𝐴 ) “ ( 𝑥 (,) +∞ ) ) = ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) )
24 cnvresima ⊢ ( ◡ ( ( ℜ ∘ 𝐹 ) ↾ 𝐴 ) “ ( 𝑥 (,) +∞ ) ) = ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 )
25 23 24 eqtr3i ⊢ ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) ) = ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 )
26 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
27 ismbfcn ⊢ ( 𝐹 : dom 𝐹 ⟶ ℂ → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )
28 26 27 syl ⊢ ( 𝐹 ∈ MblFn → ( 𝐹 ∈ MblFn ↔ ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) ) )
29 28 ibi ⊢ ( 𝐹 ∈ MblFn → ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) ∈ MblFn ) )
30 29 simpld ⊢ ( 𝐹 ∈ MblFn → ( ℜ ∘ 𝐹 ) ∈ MblFn )
31 fco ⊢ ( ( ℜ : ℂ ⟶ ℝ ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
32 1 26 31 sylancr ⊢ ( 𝐹 ∈ MblFn → ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
33 mbfima ⊢ ( ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ ) → ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
34 30 32 33 syl2anc ⊢ ( 𝐹 ∈ MblFn → ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
35 inmbl ⊢ ( ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 ) ∈ dom vol )
36 34 35 sylan ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 ) ∈ dom vol )
37 25 36 eqeltrid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
38 37 adantr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
39 22 imaeq1i ⊢ ( ◡ ( ( ℜ ∘ 𝐹 ) ↾ 𝐴 ) “ ( -∞ (,) 𝑥 ) ) = ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) )
40 cnvresima ⊢ ( ◡ ( ( ℜ ∘ 𝐹 ) ↾ 𝐴 ) “ ( -∞ (,) 𝑥 ) ) = ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 )
41 39 40 eqtr3i ⊢ ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) ) = ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 )
42 mbfima ⊢ ( ( ( ℜ ∘ 𝐹 ) ∈ MblFn ∧ ( ℜ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ ) → ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
43 30 32 42 syl2anc ⊢ ( 𝐹 ∈ MblFn → ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
44 inmbl ⊢ ( ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 ) ∈ dom vol )
45 43 44 sylan ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 ) ∈ dom vol )
46 41 45 eqeltrid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
47 46 adantr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
48 14 20 38 47 ismbf2d ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) ∈ MblFn )
49 imf ⊢ ℑ : ℂ ⟶ ℝ
50 fco ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ ) → ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℝ )
51 49 12 50 sylancr ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℝ )
52 resco ⊢ ( ( ℑ ∘ 𝐹 ) ↾ 𝐴 ) = ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) )
53 52 cnveqi ⊢ ◡ ( ( ℑ ∘ 𝐹 ) ↾ 𝐴 ) = ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) )
54 53 imaeq1i ⊢ ( ◡ ( ( ℑ ∘ 𝐹 ) ↾ 𝐴 ) “ ( 𝑥 (,) +∞ ) ) = ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) )
55 cnvresima ⊢ ( ◡ ( ( ℑ ∘ 𝐹 ) ↾ 𝐴 ) “ ( 𝑥 (,) +∞ ) ) = ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 )
56 54 55 eqtr3i ⊢ ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) ) = ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 )
57 29 simprd ⊢ ( 𝐹 ∈ MblFn → ( ℑ ∘ 𝐹 ) ∈ MblFn )
58 fco ⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
59 49 26 58 sylancr ⊢ ( 𝐹 ∈ MblFn → ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ )
60 mbfima ⊢ ( ( ( ℑ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ ) → ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
61 57 59 60 syl2anc ⊢ ( 𝐹 ∈ MblFn → ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
62 inmbl ⊢ ( ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 ) ∈ dom vol )
63 61 62 sylan ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( 𝑥 (,) +∞ ) ) ∩ 𝐴 ) ∈ dom vol )
64 56 63 eqeltrid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
65 64 adantr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( 𝑥 (,) +∞ ) ) ∈ dom vol )
66 53 imaeq1i ⊢ ( ◡ ( ( ℑ ∘ 𝐹 ) ↾ 𝐴 ) “ ( -∞ (,) 𝑥 ) ) = ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) )
67 cnvresima ⊢ ( ◡ ( ( ℑ ∘ 𝐹 ) ↾ 𝐴 ) “ ( -∞ (,) 𝑥 ) ) = ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 )
68 66 67 eqtr3i ⊢ ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) ) = ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 )
69 mbfima ⊢ ( ( ( ℑ ∘ 𝐹 ) ∈ MblFn ∧ ( ℑ ∘ 𝐹 ) : dom 𝐹 ⟶ ℝ ) → ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
70 57 59 69 syl2anc ⊢ ( 𝐹 ∈ MblFn → ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
71 inmbl ⊢ ( ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 ) ∈ dom vol )
72 70 71 sylan ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℑ ∘ 𝐹 ) “ ( -∞ (,) 𝑥 ) ) ∩ 𝐴 ) ∈ dom vol )
73 68 72 eqeltrid ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
74 73 adantr ⊢ ( ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → ( ◡ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) “ ( -∞ (,) 𝑥 ) ) ∈ dom vol )
75 51 20 65 74 ismbf2d ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) ∈ MblFn )
76 ismbfcn ⊢ ( ( 𝐹 ↾ 𝐴 ) : dom ( 𝐹 ↾ 𝐴 ) ⟶ ℂ → ( ( 𝐹 ↾ 𝐴 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) ∈ MblFn ) ) )
77 12 76 syl ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( ( 𝐹 ↾ 𝐴 ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝐹 ↾ 𝐴 ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝐹 ↾ 𝐴 ) ) ∈ MblFn ) ) )
78 48 75 77 mpbir2and ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol ) → ( 𝐹 ↾ 𝐴 ) ∈ MblFn )