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