Metamath Proof Explorer

Theorem ismbf1

Description: The predicate " F is a measurable function". This is more naturally stated for functions on the reals, see ismbf and ismbfcn for the decomposition of the real and imaginary parts. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Assertion ismbf1 ⊢ F ∈ MblFn ↔ F ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol

Proof

Step Hyp Ref Expression
1 coeq2 ⊢ f = F → ℜ ∘ f = ℜ ∘ F
2 1 cnveqd ⊢ f = F → ℜ ∘ f -1 = ℜ ∘ F -1
3 2 imaeq1d ⊢ f = F → ℜ ∘ f -1 x = ℜ ∘ F -1 x
4 3 eleq1d ⊢ f = F → ℜ ∘ f -1 x ∈ dom ⁡ vol ↔ ℜ ∘ F -1 x ∈ dom ⁡ vol
5 coeq2 ⊢ f = F → ℑ ∘ f = ℑ ∘ F
6 5 cnveqd ⊢ f = F → ℑ ∘ f -1 = ℑ ∘ F -1
7 6 imaeq1d ⊢ f = F → ℑ ∘ f -1 x = ℑ ∘ F -1 x
8 7 eleq1d ⊢ f = F → ℑ ∘ f -1 x ∈ dom ⁡ vol ↔ ℑ ∘ F -1 x ∈ dom ⁡ vol
9 4 8 anbi12d ⊢ f = F → ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol ↔ ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol
10 9 ralbidv ⊢ f = F → ∀ x ∈ ran ⁡ . ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol ↔ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol
11 df-mbf ⊢ MblFn = f ∈ ℂ ↑ 𝑝𝑚 ℝ | ∀ x ∈ ran ⁡ . ℜ ∘ f -1 x ∈ dom ⁡ vol ∧ ℑ ∘ f -1 x ∈ dom ⁡ vol
12 10 11 elrab2 ⊢ F ∈ MblFn ↔ F ∈ ℂ ↑ 𝑝𝑚 ℝ ∧ ∀ x ∈ ran ⁡ . ℜ ∘ F -1 x ∈ dom ⁡ vol ∧ ℑ ∘ F -1 x ∈ dom ⁡ vol