Theorem ismbf1 25609

Description: The predicate "𝐹 is a measurable function". This is more naturally stated for functions on the reals, see ismbf 25613 and ismbfcn 25614 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 5800	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (ℜ ∘ 𝑓) = (ℜ ∘ 𝐹))
2	1	cnveqd 5817	. . . . . 6 ⊢ (𝑓 = 𝐹 → ◡(ℜ ∘ 𝑓) = ◡(ℜ ∘ 𝐹))
3	2	imaeq1d 6011	. . . . 5 ⊢ (𝑓 = 𝐹 → (◡(ℜ ∘ 𝑓) “ 𝑥) = (◡(ℜ ∘ 𝐹) “ 𝑥))
4	3	eleq1d 2824	. . . 4 ⊢ (𝑓 = 𝐹 → ((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ↔ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol))
5		coeq2 5800	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (ℑ ∘ 𝑓) = (ℑ ∘ 𝐹))
6	5	cnveqd 5817	. . . . . 6 ⊢ (𝑓 = 𝐹 → ◡(ℑ ∘ 𝑓) = ◡(ℑ ∘ 𝐹))
7	6	imaeq1d 6011	. . . . 5 ⊢ (𝑓 = 𝐹 → (◡(ℑ ∘ 𝑓) “ 𝑥) = (◡(ℑ ∘ 𝐹) “ 𝑥))
8	7	eleq1d 2824	. . . 4 ⊢ (𝑓 = 𝐹 → ((◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol ↔ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))
9	4, 8	anbi12d 638	. . 3 ⊢ (𝑓 = 𝐹 → (((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol) ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
10	9	ralbidv 3162	. 2 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol) ↔ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))
11		df-mbf 25604	. 2 ⊢ MblFn = {𝑓 ∈ (ℂ ↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)}
12	10, 11	elrab2 3632	1 ⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ ↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ^◡ccnv 5617  dom cdm 5618  ran crn 5619   “ cima 5621   ∘ ccom 5622  (class class class)co 7356   ↑_pm cpm 8764  ℂcc 11027  ℝcr 11028  (,)cioo 13289  ℜcre 15050  ℑcim 15051  volcvol 25448  MblFncmbf 25599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-mbf 25604

This theorem is referenced by:  mbff  25610  mbfdm  25611  ismbf  25613  ismbfcn  25614  mbfconst  25618  mbfres  25629  cncombf  25643  cnmbf  25644  mbfdmssre  46443