This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )