Step | Hyp | Ref
| Expression |
1 | | mbfdm 23395 |
. . 3
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
2 | | fdm 6051 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴) |
3 | 2 | eleq1d 2686 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → (dom 𝐹 ∈ dom vol ↔ 𝐴 ∈ dom
vol)) |
4 | 1, 3 | syl5ib 234 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn → 𝐴 ∈ dom vol)) |
5 | | ioomax 12248 |
. . . . 5
⊢
(-∞(,)+∞) = ℝ |
6 | | ioorebas 12275 |
. . . . 5
⊢
(-∞(,)+∞) ∈ ran (,) |
7 | 5, 6 | eqeltrri 2698 |
. . . 4
⊢ ℝ
∈ ran (,) |
8 | | imaeq2 5462 |
. . . . . 6
⊢ (𝑥 = ℝ → (◡𝐹 “ 𝑥) = (◡𝐹 “ ℝ)) |
9 | 8 | eleq1d 2686 |
. . . . 5
⊢ (𝑥 = ℝ → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ (◡𝐹 “ ℝ) ∈ dom
vol)) |
10 | 9 | rspcv 3305 |
. . . 4
⊢ (ℝ
∈ ran (,) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → (◡𝐹 “ ℝ) ∈ dom
vol)) |
11 | 7, 10 | ax-mp 5 |
. . 3
⊢
(∀𝑥 ∈
ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → (◡𝐹 “ ℝ) ∈ dom
vol) |
12 | | fimacnv 6347 |
. . . 4
⊢ (𝐹:𝐴⟶ℝ → (◡𝐹 “ ℝ) = 𝐴) |
13 | 12 | eleq1d 2686 |
. . 3
⊢ (𝐹:𝐴⟶ℝ → ((◡𝐹 “ ℝ) ∈ dom vol ↔
𝐴 ∈ dom
vol)) |
14 | 11, 13 | syl5ib 234 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol → 𝐴 ∈ dom vol)) |
15 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
16 | 15 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℝ) |
17 | 16 | rered 13964 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐹‘𝑥)) = (𝐹‘𝑥)) |
18 | 17 | mpteq2dva 4744 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
19 | 16 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ ℂ) |
20 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹:𝐴⟶ℝ) |
21 | 20 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
22 | | ref 13852 |
. . . . . . . . . . . . . 14
⊢
ℜ:ℂ⟶ℝ |
23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) →
ℜ:ℂ⟶ℝ) |
24 | 23 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ℜ = (𝑦 ∈ ℂ ↦
(ℜ‘𝑦))) |
25 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑥) → (ℜ‘𝑦) = (ℜ‘(𝐹‘𝑥))) |
26 | 19, 21, 24, 25 | fmptco 6396 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℜ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑥)))) |
27 | 18, 26, 21 | 3eqtr4rd 2667 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 = (ℜ ∘ 𝐹)) |
28 | 27 | cnveqd 5298 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ◡𝐹 = ◡(ℜ ∘ 𝐹)) |
29 | 28 | imaeq1d 5465 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡𝐹 “ 𝑥) = (◡(ℜ ∘ 𝐹) “ 𝑥)) |
30 | 29 | eleq1d 2686 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
31 | | imf 13853 |
. . . . . . . . . . . . . . . 16
⊢
ℑ:ℂ⟶ℝ |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) →
ℑ:ℂ⟶ℝ) |
33 | 32 | feqmptd 6249 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ℑ = (𝑦 ∈ ℂ ↦
(ℑ‘𝑦))) |
34 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐹‘𝑥) → (ℑ‘𝑦) = (ℑ‘(𝐹‘𝑥))) |
35 | 19, 21, 33, 34 | fmptco 6396 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑥)))) |
36 | 16 | reim0d 13965 |
. . . . . . . . . . . . . 14
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ 𝐴) → (ℑ‘(𝐹‘𝑥)) = 0) |
37 | 36 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝑥 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐴 ↦ 0)) |
38 | 35, 37 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝑥 ∈ 𝐴 ↦ 0)) |
39 | | fconstmpt 5163 |
. . . . . . . . . . . 12
⊢ (𝐴 × {0}) = (𝑥 ∈ 𝐴 ↦ 0) |
40 | 38, 39 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (ℑ ∘
𝐹) = (𝐴 × {0})) |
41 | 40 | cnveqd 5298 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ◡(ℑ ∘ 𝐹) = ◡(𝐴 × {0})) |
42 | 41 | imaeq1d 5465 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ 𝐹) “ 𝑥) = (◡(𝐴 × {0}) “ 𝑥)) |
43 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐴 ∈ dom vol) |
44 | | 0re 10040 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
45 | | mbfconstlem 23396 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom vol ∧ 0 ∈
ℝ) → (◡(𝐴 × {0}) “ 𝑥) ∈ dom vol) |
46 | 43, 44, 45 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(𝐴 × {0}) “ 𝑥) ∈ dom vol) |
47 | 42, 46 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
48 | 47 | biantrud 528 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
49 | 30, 48 | bitrd 268 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → ((◡𝐹 “ 𝑥) ∈ dom vol ↔ ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
50 | 49 | ralbidv 2986 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol ↔ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
51 | | ax-resscn 9993 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
52 | | fss 6056 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → 𝐹:𝐴⟶ℂ) |
53 | 51, 52 | mpan2 707 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℝ → 𝐹:𝐴⟶ℂ) |
54 | | mblss 23299 |
. . . . . . 7
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
55 | | cnex 10017 |
. . . . . . . 8
⊢ ℂ
∈ V |
56 | | reex 10027 |
. . . . . . . 8
⊢ ℝ
∈ V |
57 | | elpm2r 7875 |
. . . . . . . 8
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
58 | 55, 56, 57 | mpanl12 718 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
59 | 53, 54, 58 | syl2an 494 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
60 | 59 | biantrurd 529 |
. . . . 5
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) ↔ (𝐹 ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))) |
61 | 50, 60 | bitrd 268 |
. . . 4
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol ↔ (𝐹 ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)))) |
62 | | ismbf1 23393 |
. . . 4
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ
↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
63 | 61, 62 | syl6rbbr 279 |
. . 3
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐴 ∈ dom vol) → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |
64 | 63 | ex 450 |
. 2
⊢ (𝐹:𝐴⟶ℝ → (𝐴 ∈ dom vol → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))) |
65 | 4, 14, 64 | pm5.21ndd 369 |
1
⊢ (𝐹:𝐴⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)) |