Theorem ismbf1 25501

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

Assertion

Ref	Expression
ismbf1	⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))

Distinct variable group:   𝑥,𝐹

Proof of Theorem ismbf1

Dummy variable 𝑓 is distinct from all other variables.

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ^◡ccnv 5630  dom cdm 5631  ran crn 5632   “ cima 5634   ∘ ccom 5635  (class class class)co 7369   ↑_pm cpm 8777  ℂcc 11042  ℝcr 11043  (,)cioo 13282  ℜcre 15039  ℑcim 15040  volcvol 25340  MblFncmbf 25491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-mbf 25496

This theorem is referenced by:  mbff  25502  mbfdm  25503  ismbf  25505  ismbfcn  25506  mbfconst  25510  mbfres  25521  cncombf  25535  cnmbf  25536  mbfdmssre  45971