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 ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )

Proof

Step Hyp Ref Expression
1 coeq2 ( 𝑓 = 𝐹 → ( ℜ ∘ 𝑓 ) = ( ℜ ∘ 𝐹 ) )
2 1 cnveqd ( 𝑓 = 𝐹 ( ℜ ∘ 𝑓 ) = ( ℜ ∘ 𝐹 ) )
3 2 imaeq1d ( 𝑓 = 𝐹 → ( ( ℜ ∘ 𝑓 ) “ 𝑥 ) = ( ( ℜ ∘ 𝐹 ) “ 𝑥 ) )
4 3 eleq1d ( 𝑓 = 𝐹 → ( ( ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ↔ ( ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) )
5 coeq2 ( 𝑓 = 𝐹 → ( ℑ ∘ 𝑓 ) = ( ℑ ∘ 𝐹 ) )
6 5 cnveqd ( 𝑓 = 𝐹 ( ℑ ∘ 𝑓 ) = ( ℑ ∘ 𝐹 ) )
7 6 imaeq1d ( 𝑓 = 𝐹 → ( ( ℑ ∘ 𝑓 ) “ 𝑥 ) = ( ( ℑ ∘ 𝐹 ) “ 𝑥 ) )
8 7 eleq1d ( 𝑓 = 𝐹 → ( ( ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ↔ ( ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) )
9 4 8 anbi12d ( 𝑓 = 𝐹 → ( ( ( ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ) ↔ ( ( ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
10 9 ralbidv ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ ran (,) ( ( ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ) ↔ ∀ 𝑥 ∈ ran (,) ( ( ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )
11 df-mbf MblFn = { 𝑓 ∈ ( ℂ ↑pm ℝ ) ∣ ∀ 𝑥 ∈ ran (,) ( ( ( ℜ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝑓 ) “ 𝑥 ) ∈ dom vol ) }
12 10 11 elrab2 ( 𝐹 ∈ MblFn ↔ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑥 ∈ ran (,) ( ( ( ℜ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ∧ ( ( ℑ ∘ 𝐹 ) “ 𝑥 ) ∈ dom vol ) ) )