Step | Hyp | Ref
| Expression |
1 | | ref 14751 |
. . . 4
⊢
ℜ:ℂ⟶ℝ |
2 | | simpr 484 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → 𝐴 ∈ dom
vol) |
3 | | ismbf1 24693 |
. . . . . . . . 9
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ
↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
4 | 3 | simplbi 497 |
. . . . . . . 8
⊢ (𝐹 ∈ MblFn → 𝐹 ∈ (ℂ
↑pm ℝ)) |
5 | 4 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → 𝐹 ∈ (ℂ
↑pm ℝ)) |
6 | | pmresg 8616 |
. . . . . . 7
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (ℂ
↑pm ℝ)) → (𝐹 ↾ 𝐴) ∈ (ℂ ↑pm 𝐴)) |
7 | 2, 5, 6 | syl2anc 583 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴) ∈ (ℂ ↑pm 𝐴)) |
8 | | cnex 10883 |
. . . . . . 7
⊢ ℂ
∈ V |
9 | | elpm2g 8590 |
. . . . . . 7
⊢ ((ℂ
∈ V ∧ 𝐴 ∈ dom
vol) → ((𝐹 ↾
𝐴) ∈ (ℂ
↑pm 𝐴)
↔ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ 𝐴))) |
10 | 8, 2, 9 | sylancr 586 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((𝐹 ↾ 𝐴) ∈ (ℂ ↑pm 𝐴) ↔ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ 𝐴))) |
11 | 7, 10 | mpbid 231 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ 𝐴)) |
12 | 11 | simpld 494 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ) |
13 | | fco 6608 |
. . . 4
⊢
((ℜ:ℂ⟶ℝ ∧ (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ) → (ℜ ∘
(𝐹 ↾ 𝐴)):dom (𝐹 ↾ 𝐴)⟶ℝ) |
14 | 1, 12, 13 | sylancr 586 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (ℜ
∘ (𝐹 ↾ 𝐴)):dom (𝐹 ↾ 𝐴)⟶ℝ) |
15 | | dmres 5902 |
. . . 4
⊢ dom
(𝐹 ↾ 𝐴) = (𝐴 ∩ dom 𝐹) |
16 | | id 22 |
. . . . 5
⊢ (𝐴 ∈ dom vol → 𝐴 ∈ dom
vol) |
17 | | mbfdm 24695 |
. . . . 5
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
18 | | inmbl 24611 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ dom 𝐹 ∈ dom vol) → (𝐴 ∩ dom 𝐹) ∈ dom vol) |
19 | 16, 17, 18 | syl2anr 596 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐴 ∩ dom 𝐹) ∈ dom vol) |
20 | 15, 19 | eqeltrid 2843 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → dom
(𝐹 ↾ 𝐴) ∈ dom
vol) |
21 | | resco 6143 |
. . . . . . . 8
⊢ ((ℜ
∘ 𝐹) ↾ 𝐴) = (ℜ ∘ (𝐹 ↾ 𝐴)) |
22 | 21 | cnveqi 5772 |
. . . . . . 7
⊢ ◡((ℜ ∘ 𝐹) ↾ 𝐴) = ◡(ℜ ∘ (𝐹 ↾ 𝐴)) |
23 | 22 | imaeq1i 5955 |
. . . . . 6
⊢ (◡((ℜ ∘ 𝐹) ↾ 𝐴) “ (𝑥(,)+∞)) = (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) |
24 | | cnvresima 6122 |
. . . . . 6
⊢ (◡((ℜ ∘ 𝐹) ↾ 𝐴) “ (𝑥(,)+∞)) = ((◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) |
25 | 23, 24 | eqtr3i 2768 |
. . . . 5
⊢ (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) = ((◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) |
26 | | mbff 24694 |
. . . . . . . . . 10
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
27 | | ismbfcn 24698 |
. . . . . . . . . 10
⊢ (𝐹:dom 𝐹⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn))) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝐹 ∈ MblFn → (𝐹 ∈ MblFn ↔ ((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℑ ∘ 𝐹)
∈ MblFn))) |
29 | 28 | ibi 266 |
. . . . . . . 8
⊢ (𝐹 ∈ MblFn → ((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℑ ∘ 𝐹)
∈ MblFn)) |
30 | 29 | simpld 494 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → (ℜ
∘ 𝐹) ∈
MblFn) |
31 | | fco 6608 |
. . . . . . . 8
⊢
((ℜ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℜ ∘
𝐹):dom 𝐹⟶ℝ) |
32 | 1, 26, 31 | sylancr 586 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → (ℜ
∘ 𝐹):dom 𝐹⟶ℝ) |
33 | | mbfima 24699 |
. . . . . . 7
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):dom 𝐹⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∈ dom
vol) |
34 | 30, 32, 33 | syl2anc 583 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → (◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∈ dom
vol) |
35 | | inmbl 24611 |
. . . . . 6
⊢ (((◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∈ dom vol ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) ∈ dom vol) |
36 | 34, 35 | sylan 579 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) ∈ dom vol) |
37 | 25, 36 | eqeltrid 2843 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) ∈ dom
vol) |
38 | 37 | adantr 480 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ ℝ) → (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) ∈ dom
vol) |
39 | 22 | imaeq1i 5955 |
. . . . . 6
⊢ (◡((ℜ ∘ 𝐹) ↾ 𝐴) “ (-∞(,)𝑥)) = (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) |
40 | | cnvresima 6122 |
. . . . . 6
⊢ (◡((ℜ ∘ 𝐹) ↾ 𝐴) “ (-∞(,)𝑥)) = ((◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) |
41 | 39, 40 | eqtr3i 2768 |
. . . . 5
⊢ (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) = ((◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) |
42 | | mbfima 24699 |
. . . . . . 7
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):dom 𝐹⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∈ dom vol) |
43 | 30, 32, 42 | syl2anc 583 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → (◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∈ dom vol) |
44 | | inmbl 24611 |
. . . . . 6
⊢ (((◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∈ dom vol ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) ∈ dom vol) |
45 | 43, 44 | sylan 579 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((◡(ℜ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) ∈ dom vol) |
46 | 41, 45 | eqeltrid 2843 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) ∈ dom vol) |
47 | 46 | adantr 480 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ ℝ) → (◡(ℜ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) ∈ dom vol) |
48 | 14, 20, 38, 47 | ismbf2d 24709 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (ℜ
∘ (𝐹 ↾ 𝐴)) ∈
MblFn) |
49 | | imf 14752 |
. . . 4
⊢
ℑ:ℂ⟶ℝ |
50 | | fco 6608 |
. . . 4
⊢
((ℑ:ℂ⟶ℝ ∧ (𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ) → (ℑ ∘
(𝐹 ↾ 𝐴)):dom (𝐹 ↾ 𝐴)⟶ℝ) |
51 | 49, 12, 50 | sylancr 586 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (ℑ
∘ (𝐹 ↾ 𝐴)):dom (𝐹 ↾ 𝐴)⟶ℝ) |
52 | | resco 6143 |
. . . . . . . 8
⊢ ((ℑ
∘ 𝐹) ↾ 𝐴) = (ℑ ∘ (𝐹 ↾ 𝐴)) |
53 | 52 | cnveqi 5772 |
. . . . . . 7
⊢ ◡((ℑ ∘ 𝐹) ↾ 𝐴) = ◡(ℑ ∘ (𝐹 ↾ 𝐴)) |
54 | 53 | imaeq1i 5955 |
. . . . . 6
⊢ (◡((ℑ ∘ 𝐹) ↾ 𝐴) “ (𝑥(,)+∞)) = (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) |
55 | | cnvresima 6122 |
. . . . . 6
⊢ (◡((ℑ ∘ 𝐹) ↾ 𝐴) “ (𝑥(,)+∞)) = ((◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) |
56 | 54, 55 | eqtr3i 2768 |
. . . . 5
⊢ (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) = ((◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) |
57 | 29 | simprd 495 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → (ℑ
∘ 𝐹) ∈
MblFn) |
58 | | fco 6608 |
. . . . . . . 8
⊢
((ℑ:ℂ⟶ℝ ∧ 𝐹:dom 𝐹⟶ℂ) → (ℑ ∘
𝐹):dom 𝐹⟶ℝ) |
59 | 49, 26, 58 | sylancr 586 |
. . . . . . 7
⊢ (𝐹 ∈ MblFn → (ℑ
∘ 𝐹):dom 𝐹⟶ℝ) |
60 | | mbfima 24699 |
. . . . . . 7
⊢
(((ℑ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹):dom 𝐹⟶ℝ) → (◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∈ dom
vol) |
61 | 57, 59, 60 | syl2anc 583 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → (◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∈ dom
vol) |
62 | | inmbl 24611 |
. . . . . 6
⊢ (((◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∈ dom vol ∧ 𝐴 ∈ dom vol) → ((◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) ∈ dom vol) |
63 | 61, 62 | sylan 579 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((◡(ℑ ∘ 𝐹) “ (𝑥(,)+∞)) ∩ 𝐴) ∈ dom vol) |
64 | 56, 63 | eqeltrid 2843 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) ∈ dom
vol) |
65 | 64 | adantr 480 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ ℝ) → (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (𝑥(,)+∞)) ∈ dom
vol) |
66 | 53 | imaeq1i 5955 |
. . . . . 6
⊢ (◡((ℑ ∘ 𝐹) ↾ 𝐴) “ (-∞(,)𝑥)) = (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) |
67 | | cnvresima 6122 |
. . . . . 6
⊢ (◡((ℑ ∘ 𝐹) ↾ 𝐴) “ (-∞(,)𝑥)) = ((◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) |
68 | 66, 67 | eqtr3i 2768 |
. . . . 5
⊢ (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) = ((◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) |
69 | | mbfima 24699 |
. . . . . . 7
⊢
(((ℑ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹):dom 𝐹⟶ℝ) → (◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∈ dom vol) |
70 | 57, 59, 69 | syl2anc 583 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → (◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∈ dom vol) |
71 | | inmbl 24611 |
. . . . . 6
⊢ (((◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∈ dom vol ∧ 𝐴 ∈ dom vol) → ((◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) ∈ dom vol) |
72 | 70, 71 | sylan 579 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((◡(ℑ ∘ 𝐹) “ (-∞(,)𝑥)) ∩ 𝐴) ∈ dom vol) |
73 | 68, 72 | eqeltrid 2843 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) ∈ dom vol) |
74 | 73 | adantr 480 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) ∧ 𝑥 ∈ ℝ) → (◡(ℑ ∘ (𝐹 ↾ 𝐴)) “ (-∞(,)𝑥)) ∈ dom vol) |
75 | 51, 20, 65, 74 | ismbf2d 24709 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (ℑ
∘ (𝐹 ↾ 𝐴)) ∈
MblFn) |
76 | | ismbfcn 24698 |
. . 3
⊢ ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ → ((𝐹 ↾ 𝐴) ∈ MblFn ↔ ((ℜ ∘
(𝐹 ↾ 𝐴)) ∈ MblFn ∧ (ℑ
∘ (𝐹 ↾ 𝐴)) ∈
MblFn))) |
77 | 12, 76 | syl 17 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → ((𝐹 ↾ 𝐴) ∈ MblFn ↔ ((ℜ ∘
(𝐹 ↾ 𝐴)) ∈ MblFn ∧ (ℑ
∘ (𝐹 ↾ 𝐴)) ∈
MblFn))) |
78 | 48, 75, 77 | mpbir2and 709 |
1
⊢ ((𝐹 ∈ MblFn ∧ 𝐴 ∈ dom vol) → (𝐹 ↾ 𝐴) ∈ MblFn) |