# 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$