Metamath Proof Explorer

Theorem 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 ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )

Proof

Step Hyp Ref Expression
1 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
2 fdm ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → dom 𝐹 = 𝐴 )
3 2 eleq1d ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( dom 𝐹 ∈ dom vol ↔ 𝐴 ∈ dom vol ) )
4 1 3 syl5ib ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn → 𝐴 ∈ dom vol ) )
5 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
6 ioorebas ⊢ ( -∞ (,) +∞ ) ∈ ran (,)
7 5 6 eqeltrri ⊢ ℝ ∈ ran (,)
8 imaeq2 ⊢ ( 𝑥 = ℝ → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ ℝ ) )
9 8 eleq1d ⊢ ( 𝑥 = ℝ → ( ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ↔ ( ◡ 𝐹 “ ℝ ) ∈ dom vol ) )
10 9 rspcv ⊢ ( ℝ ∈ ran (,) → ( ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol → ( ◡ 𝐹 “ ℝ ) ∈ dom vol ) )
11 7 10 ax-mp ⊢ ( ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol → ( ◡ 𝐹 “ ℝ ) ∈ dom vol )
12 fimacnv ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( ◡ 𝐹 “ ℝ ) = 𝐴 )
13 12 eleq1d ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( ( ◡ 𝐹 “ ℝ ) ∈ dom vol ↔ 𝐴 ∈ dom vol ) )
14 11 13 syl5ib ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol → 𝐴 ∈ dom vol ) )
15 ismbf1 ⊢ ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
16 ffvelrn ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
17 16 adantlr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
18 17 rered ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
19 18 mpteq2dva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
20 17 recnd ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
21 simpl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → 𝐹 : 𝐴 ⟶ ℝ )
22 21 feqmptd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
23 ref ⊢ ℜ : ℂ ⟶ ℝ
24 23 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ℜ : ℂ ⟶ ℝ )
25 24 feqmptd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ℜ = ( 𝑦 ∈ ℂ ↦ ( ℜ ‘ 𝑦 ) ) )
26 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ℜ ‘ 𝑦 ) = ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) )
27 20 22 25 26 fmptco ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ℜ ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
28 19 27 22 3eqtr4rd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → 𝐹 = ( ℜ ∘ 𝐹 ) )
29 28 cnveqd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ◡ 𝐹 = ◡ ( ℜ ∘ 𝐹 ) )
30 29 imaeq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) )
31 30 eleq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ↔ ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) )
32 imf ⊢ ℑ : ℂ ⟶ ℝ
33 32 a1i ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ℑ : ℂ ⟶ ℝ )
34 33 feqmptd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ℑ = ( 𝑦 ∈ ℂ ↦ ( ℑ ‘ 𝑦 ) ) )
35 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ℑ ‘ 𝑦 ) = ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) )
36 20 22 34 35 fmptco ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ℑ ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
37 17 reim0d ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) = 0 )
38 37 mpteq2dva ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
39 36 38 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ℑ ∘ 𝐹 ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
40 fconstmpt ⊢ ( 𝐴 × { 0 } ) = ( 𝑥 ∈ 𝐴 ↦ 0 )
41 39 40 eqtr4di ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ℑ ∘ 𝐹 ) = ( 𝐴 × { 0 } ) )
42 41 cnveqd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ◡ ( ℑ ∘ 𝐹 ) = ◡ ( 𝐴 × { 0 } ) )
43 42 imaeq1d ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) = ( ◡ ( 𝐴 × { 0 } ) “ 𝑥 ) )
44 simpr ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → 𝐴 ∈ dom vol )
45 0re ⊢ 0 ∈ ℝ
46 mbfconstlem ⊢ ( ( 𝐴 ∈ dom vol ∧ 0 ∈ ℝ ) → ( ◡ ( 𝐴 × { 0 } ) “ 𝑥 ) ∈ dom vol )
47 44 45 46 sylancl ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ◡ ( 𝐴 × { 0 } ) “ 𝑥 ) ∈ dom vol )
48 43 47 eqeltrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol )
49 48 biantrud ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ↔ ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
50 31 49 bitrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ↔ ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
51 50 ralbidv ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ↔ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
52 ax-resscn ⊢ ℝ ⊆ ℂ
53 fss ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
54 52 53 mpan2 ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → 𝐹 : 𝐴 ⟶ ℂ )
55 mblss ⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
56 cnex ⊢ ℂ ∈ V
57 reex ⊢ ℝ ∈ V
58 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
59 56 57 58 mpanl12 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
60 54 55 59 syl2an ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
61 60 biantrurd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) ) )
62 51 61 bitrd ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ◡ ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) ) )
63 15 62 bitr4id ⊢ ( ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ∈ dom vol ) → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
64 63 ex ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐴 ∈ dom vol → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) ) )
65 4 14 64 pm5.21ndd ⊢ ( 𝐹 : 𝐴 ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )