Step | Hyp | Ref
| Expression |
1 | | mbfdm 24230 |
. . 3
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
2 | | fdm 6495 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
3 | 2 | eleq1d 2874 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (dom 𝐹 ∈ dom vol ↔ 𝐴 ∈ dom
vol)) |
4 | 1, 3 | syl5ib 247 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn → 𝐴 ∈ dom vol)) |
5 | | ioomax 12800 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
6 | | ioorebas 12829 |
. . . . 5
⊢
(-∞(,)+∞) ∈ ran (,) |
7 | 5, 6 | eqeltrri 2887 |
. . . 4
⊢ ℝ
∈ ran (,) |
8 | | imaeq2 5892 |
. . . . . 6
⊢ (𝑥 = ℝ → (◡𝐹 “ 𝑥) = (◡𝐹 “ ℝ)) |
9 | 8 | eleq1d 2874 |
. . . . 5
⊢ (𝑥 = ℝ → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ (◡𝐹 “ ℝ) ∈ dom
vol)) |
10 | 9 | rspcv 3566 |
. . . 4
⊢ (ℝ
∈ ran (,) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → (◡𝐹 “ ℝ) ∈ dom
vol)) |
11 | 7, 10 | ax-mp 5 |
. . 3
⊢
(∀𝑥 ∈
ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → (◡𝐹 “ ℝ) ∈ dom
vol) |
12 | | fimacnv 6816 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ ℝ) = 𝐴) |
13 | 12 | eleq1d 2874 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → ((◡𝐹 “ ℝ) ∈ dom vol ↔
𝐴 ∈ dom
vol)) |
14 | 11, 13 | syl5ib 247 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → 𝐴 ∈ dom vol)) |
15 | | ismbf1 24228 |
. . . 4
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ
↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
16 | | ffvelrn 6826 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
17 | 16 | adantlr 714 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
18 | 17 | rered 14575 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
19 | 18 | mpteq2dva 5125 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
20 | 17 | recnd 10658 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
21 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹:𝐴⟶ℝ) |
22 | 21 | feqmptd 6708 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
23 | | ref 14463 |
. . . . . . . . . . . . . 14
⊢
ℜ:ℂ⟶ℝ |
24 | 23 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) →
ℜ:ℂ⟶ℝ) |
25 | 24 | feqmptd 6708 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ℜ = (𝑦 ∈ ℂ ↦
(ℜ‘𝑦))) |
26 | | fveq2 6645 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑥) → (ℜ‘𝑦) = (ℜ‘(𝐹‘𝑥))) |
27 | 20, 22, 25, 26 | fmptco 6868 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℜ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑥)))) |
28 | 19, 27, 22 | 3eqtr4rd 2844 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 = (ℜ ∘ 𝐹)) |
29 | 28 | cnveqd 5710 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ◡𝐹 = ◡(ℜ ∘ 𝐹)) |
30 | 29 | imaeq1d 5895 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡𝐹 “ 𝑥) = (◡(ℜ ∘ 𝐹) “ 𝑥)) |
31 | 30 | eleq1d 2874 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
32 | | imf 14464 |
. . . . . . . . . . . . . . . 16
⊢
ℑ:ℂ⟶ℝ |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) →
ℑ:ℂ⟶ℝ) |
34 | 33 | feqmptd 6708 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ℑ = (𝑦 ∈ ℂ ↦
(ℑ‘𝑦))) |
35 | | fveq2 6645 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐹‘𝑥) → (ℑ‘𝑦) = (ℑ‘(𝐹‘𝑥))) |
36 | 20, 22, 34, 35 | fmptco 6868 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑥)))) |
37 | 17 | reim0d 14576 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐹‘𝑥)) = 0) |
38 | 37 | mpteq2dva 5125 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ 0)) |
39 | 36, 38 | eqtrd 2833 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ 0)) |
40 | | fconstmpt 5578 |
. . . . . . . . . . . 12
⊢ (𝐴 × {0}) = (𝑥 ∈ 𝐴 ↦ 0) |
41 | 39, 40 | eqtr4di 2851 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝐴 × {0})) |
42 | 41 | cnveqd 5710 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ◡(ℑ ∘ 𝐹) = ◡(𝐴 × {0})) |
43 | 42 | imaeq1d 5895 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ 𝐹) “ 𝑥) = (◡(𝐴 × {0}) “ 𝑥)) |
44 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐴 ∈ dom vol) |
45 | | 0re 10632 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
46 | | mbfconstlem 24231 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 0 ∈
ℝ) → (◡(𝐴 × {0}) “ 𝑥) ∈ dom vol) |
47 | 44, 45, 46 | sylancl 589 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(𝐴 × {0}) “ 𝑥) ∈ dom vol) |
48 | 43, 47 | eqeltrd 2890 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
49 | 48 | biantrud 535 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
50 | 31, 49 | bitrd 282 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
51 | 50 | ralbidv 3162 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol ↔ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
52 | | ax-resscn 10583 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
53 | | fss 6501 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
54 | 52, 53 | mpan2 690 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℂ) |
55 | | mblss 24135 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
56 | | cnex 10607 |
. . . . . . . 8
⊢ ℂ
∈ V |
57 | | reex 10617 |
. . . . . . . 8
⊢ ℝ
∈ V |
58 | | elpm2r 8407 |
. . . . . . . 8
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
59 | 56, 57, 58 | mpanl12 701 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
60 | 54, 55, 59 | syl2an 598 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
61 | 60 | biantrurd 536 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) ↔ (𝐹 ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))) |
62 | 51, 61 | bitrd 282 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol ↔ (𝐹 ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))) |
63 | 15, 62 | bitr4id 293 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
64 | 63 | ex 416 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (𝐴 ∈ dom vol → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))) |
65 | 4, 14, 64 | pm5.21ndd 384 |
1
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |