Step | Hyp | Ref
| Expression |
1 | | mbfdm 24771 |
. . 3
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
2 | | fdm 6605 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
3 | 2 | eleq1d 2824 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (dom 𝐹 ∈ dom vol ↔ 𝐴 ∈ dom
vol)) |
4 | 1, 3 | syl5ib 243 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn → 𝐴 ∈ dom vol)) |
5 | | ioomax 13136 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
6 | | ioorebas 13165 |
. . . . 5
⊢
(-∞(,)+∞) ∈ ran (,) |
7 | 5, 6 | eqeltrri 2837 |
. . . 4
⊢ ℝ
∈ ran (,) |
8 | | imaeq2 5962 |
. . . . . 6
⊢ (𝑥 = ℝ → (◡𝐹 “ 𝑥) = (◡𝐹 “ ℝ)) |
9 | 8 | eleq1d 2824 |
. . . . 5
⊢ (𝑥 = ℝ → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ (◡𝐹 “ ℝ) ∈ dom
vol)) |
10 | 9 | rspcv 3555 |
. . . 4
⊢ (ℝ
∈ ran (,) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → (◡𝐹 “ ℝ) ∈ dom
vol)) |
11 | 7, 10 | ax-mp 5 |
. . 3
⊢
(∀𝑥 ∈
ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → (◡𝐹 “ ℝ) ∈ dom
vol) |
12 | | fimacnv 6618 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ ℝ) = 𝐴) |
13 | 12 | eleq1d 2824 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → ((◡𝐹 “ ℝ) ∈ dom vol ↔
𝐴 ∈ dom
vol)) |
14 | 11, 13 | syl5ib 243 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → 𝐴 ∈ dom vol)) |
15 | | ismbf1 24769 |
. . . 4
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ
↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
16 | | ffvelrn 6953 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
17 | 16 | adantlr 711 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
18 | 17 | rered 14916 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
19 | 18 | mpteq2dva 5178 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
20 | 17 | recnd 10987 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
21 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹:𝐴⟶ℝ) |
22 | 21 | feqmptd 6831 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
23 | | ref 14804 |
. . . . . . . . . . . . . 14
⊢
ℜ:ℂ⟶ℝ |
24 | 23 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) →
ℜ:ℂ⟶ℝ) |
25 | 24 | feqmptd 6831 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ℜ = (𝑦 ∈ ℂ ↦
(ℜ‘𝑦))) |
26 | | fveq2 6768 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑥) → (ℜ‘𝑦) = (ℜ‘(𝐹‘𝑥))) |
27 | 20, 22, 25, 26 | fmptco 6995 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℜ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑥)))) |
28 | 19, 27, 22 | 3eqtr4rd 2790 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 = (ℜ ∘ 𝐹)) |
29 | 28 | cnveqd 5781 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ◡𝐹 = ◡(ℜ ∘ 𝐹)) |
30 | 29 | imaeq1d 5965 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡𝐹 “ 𝑥) = (◡(ℜ ∘ 𝐹) “ 𝑥)) |
31 | 30 | eleq1d 2824 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
32 | | imf 14805 |
. . . . . . . . . . . . . . . 16
⊢
ℑ:ℂ⟶ℝ |
33 | 32 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) →
ℑ:ℂ⟶ℝ) |
34 | 33 | feqmptd 6831 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ℑ = (𝑦 ∈ ℂ ↦
(ℑ‘𝑦))) |
35 | | fveq2 6768 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐹‘𝑥) → (ℑ‘𝑦) = (ℑ‘(𝐹‘𝑥))) |
36 | 20, 22, 34, 35 | fmptco 6995 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑥)))) |
37 | 17 | reim0d 14917 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐹‘𝑥)) = 0) |
38 | 37 | mpteq2dva 5178 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ 0)) |
39 | 36, 38 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ 0)) |
40 | | fconstmpt 5648 |
. . . . . . . . . . . 12
⊢ (𝐴 × {0}) = (𝑥 ∈ 𝐴 ↦ 0) |
41 | 39, 40 | eqtr4di 2797 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝐴 × {0})) |
42 | 41 | cnveqd 5781 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ◡(ℑ ∘ 𝐹) = ◡(𝐴 × {0})) |
43 | 42 | imaeq1d 5965 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ 𝐹) “ 𝑥) = (◡(𝐴 × {0}) “ 𝑥)) |
44 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐴 ∈ dom vol) |
45 | | 0re 10961 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
46 | | mbfconstlem 24772 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 0 ∈
ℝ) → (◡(𝐴 × {0}) “ 𝑥) ∈ dom vol) |
47 | 44, 45, 46 | sylancl 585 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(𝐴 × {0}) “ 𝑥) ∈ dom vol) |
48 | 43, 47 | eqeltrd 2840 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
49 | 48 | biantrud 531 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
50 | 31, 49 | bitrd 278 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
51 | 50 | ralbidv 3122 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol ↔ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
52 | | ax-resscn 10912 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
53 | | fss 6613 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
54 | 52, 53 | mpan2 687 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℂ) |
55 | | mblss 24676 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
56 | | cnex 10936 |
. . . . . . . 8
⊢ ℂ
∈ V |
57 | | reex 10946 |
. . . . . . . 8
⊢ ℝ
∈ V |
58 | | elpm2r 8607 |
. . . . . . . 8
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
59 | 56, 57, 58 | mpanl12 698 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
60 | 54, 55, 59 | syl2an 595 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
61 | 60 | biantrurd 532 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) ↔ (𝐹 ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))) |
62 | 51, 61 | bitrd 278 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol ↔ (𝐹 ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))) |
63 | 15, 62 | bitr4id 289 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
64 | 63 | ex 412 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (𝐴 ∈ dom vol → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))) |
65 | 4, 14, 64 | pm5.21ndd 380 |
1
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |