Step | Hyp | Ref
| Expression |
1 | | elpri 4197 |
. . 3
⊢ (𝐺 ∈ {ℜ, ℑ} →
(𝐺 = ℜ ∨ 𝐺 = ℑ)) |
2 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝐺 = ℜ → (𝐺‘(𝐹‘𝑡)) = (ℜ‘(𝐹‘𝑡))) |
3 | 2 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝐺 = ℜ →
(abs‘(𝐺‘(𝐹‘𝑡))) = (abs‘(ℜ‘(𝐹‘𝑡)))) |
4 | 3 | ifeq1d 4104 |
. . . . . . . 8
⊢ (𝐺 = ℜ → if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0) = if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) |
5 | 4 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝐺 = ℜ → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) |
6 | 5 | fveq2d 6195 |
. . . . . 6
⊢ (𝐺 = ℜ →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))) |
7 | 6 | adantl 482 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℜ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))) |
8 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (𝐹‘𝑡) ∈ ℂ) |
9 | 8 | recld 13934 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ) |
10 | 9 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝑡 ∈ 𝐴) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ) |
11 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹:𝐴⟶ℂ) |
12 | 11 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹 = (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡))) |
13 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹 ∈
𝐿1) |
14 | 12, 13 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
15 | 8 | iblcn 23565 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1))) |
16 | 15 | biimpa 501 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1)) |
17 | 14, 16 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1)) |
18 | 17 | simpld 475 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈
𝐿1) |
19 | 9 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ) |
20 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) |
21 | | absf 14077 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
22 | 21 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴⟶ℂ →
abs:ℂ⟶ℝ) |
23 | 22 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → abs = (𝑥 ∈ ℂ ↦
(abs‘𝑥))) |
24 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ℜ‘(𝐹‘𝑡)) → (abs‘𝑥) = (abs‘(ℜ‘(𝐹‘𝑡)))) |
25 | 19, 20, 23, 24 | fmptco 6396 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℂ → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡))))) |
26 | 25 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡))))) |
27 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) |
28 | 9, 27 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
29 | 28 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
30 | | iblmbf 23534 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹 ∈ MblFn) |
32 | 12, 31 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ MblFn) |
33 | 8 | ismbfcn2 23406 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))) |
34 | 33 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ MblFn) → ((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
35 | 32, 34 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
36 | 35 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) |
37 | | ftc1anclem1 33485 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))):𝐴⟶ℝ ∧ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) ∈ MblFn) |
38 | 29, 36, 37 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) ∈ MblFn) |
39 | 26, 38 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn) |
40 | 10, 18, 39 | iblabsnc 33474 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡)))) ∈
𝐿1) |
41 | 19 | abscld 14175 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ) |
42 | 19 | absge0d 14183 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → 0 ≤
(abs‘(ℜ‘(𝐹‘𝑡)))) |
43 | 41, 42 | iblpos 23559 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
44 | 43 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
45 | 40, 44 | mpbid 222 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)) |
46 | 45 | simprd 479 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
47 | 46 | adantr 481 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℜ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
48 | 7, 47 | eqeltrd 2701 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℜ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
49 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝐺 = ℑ → (𝐺‘(𝐹‘𝑡)) = (ℑ‘(𝐹‘𝑡))) |
50 | 49 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝐺 = ℑ →
(abs‘(𝐺‘(𝐹‘𝑡))) = (abs‘(ℑ‘(𝐹‘𝑡)))) |
51 | 50 | ifeq1d 4104 |
. . . . . . . 8
⊢ (𝐺 = ℑ → if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0) = if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) |
52 | 51 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝐺 = ℑ → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) |
53 | 52 | fveq2d 6195 |
. . . . . 6
⊢ (𝐺 = ℑ →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
54 | 53 | adantl 482 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℑ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
55 | 8 | imcld 13935 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ) |
56 | 55 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ) |
57 | 56 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝑡 ∈ 𝐴) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ) |
58 | 17 | simprd 479 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1) |
59 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) |
60 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ℑ‘(𝐹‘𝑡)) → (abs‘𝑥) = (abs‘(ℑ‘(𝐹‘𝑡)))) |
61 | 56, 59, 23, 60 | fmptco 6396 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℂ → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡))))) |
62 | 61 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡))))) |
63 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) |
64 | 55, 63 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
65 | 64 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
66 | 35 | simprd 479 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn) |
67 | | ftc1anclem1 33485 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))):𝐴⟶ℝ ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) ∈ MblFn) |
68 | 65, 66, 67 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) ∈ MblFn) |
69 | 62, 68 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn) |
70 | 57, 58, 69 | iblabsnc 33474 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡)))) ∈
𝐿1) |
71 | 56 | abscld 14175 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ) |
72 | 56 | absge0d 14183 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → 0 ≤
(abs‘(ℑ‘(𝐹‘𝑡)))) |
73 | 71, 72 | iblpos 23559 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
74 | 73 | adantr 481 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
75 | 70, 74 | mpbid 222 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)) |
76 | 75 | simprd 479 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
77 | 76 | adantr 481 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℑ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
78 | 54, 77 | eqeltrd 2701 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℑ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
79 | 48, 78 | jaodan 826 |
. . 3
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ (𝐺 = ℜ ∨ 𝐺 = ℑ)) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
80 | 1, 79 | sylan2 491 |
. 2
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 ∈ {ℜ, ℑ})
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
81 | 80 | 3impa 1259 |
1
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ 𝐺 ∈ {ℜ, ℑ})
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |