| Step | Hyp | Ref
| Expression |
| 1 | | elpri 4649 |
. . 3
⊢ (𝐺 ∈ {ℜ, ℑ} →
(𝐺 = ℜ ∨ 𝐺 = ℑ)) |
| 2 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝐺 = ℜ → (𝐺‘(𝐹‘𝑡)) = (ℜ‘(𝐹‘𝑡))) |
| 3 | 2 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝐺 = ℜ →
(abs‘(𝐺‘(𝐹‘𝑡))) = (abs‘(ℜ‘(𝐹‘𝑡)))) |
| 4 | 3 | ifeq1d 4545 |
. . . . . . . 8
⊢ (𝐺 = ℜ → if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0) = if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) |
| 5 | 4 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝐺 = ℜ → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) |
| 6 | 5 | fveq2d 6910 |
. . . . . 6
⊢ (𝐺 = ℜ →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℜ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℜ‘(𝐹‘𝑡))), 0)))) |
| 8 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (𝐹‘𝑡) ∈ ℂ) |
| 9 | 8 | recld 15233 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ) |
| 10 | 9 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝑡 ∈ 𝐴) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ) |
| 11 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹:𝐴⟶ℂ) |
| 12 | 11 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹 = (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡))) |
| 13 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹 ∈
𝐿1) |
| 14 | 12, 13 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
| 15 | 8 | iblcn 25834 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1))) |
| 16 | 15 | biimpa 476 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1)) |
| 17 | 14, 16 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1)) |
| 18 | 17 | simpld 494 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈
𝐿1) |
| 19 | 9 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ) |
| 20 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) |
| 21 | | absf 15376 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
| 22 | 21 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴⟶ℂ →
abs:ℂ⟶ℝ) |
| 23 | 22 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → abs = (𝑥 ∈ ℂ ↦
(abs‘𝑥))) |
| 24 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ℜ‘(𝐹‘𝑡)) → (abs‘𝑥) = (abs‘(ℜ‘(𝐹‘𝑡)))) |
| 25 | 19, 20, 23, 24 | fmptco 7149 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℂ → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡))))) |
| 26 | 25 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡))))) |
| 27 | 9 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
| 29 | | iblmbf 25802 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → 𝐹 ∈ MblFn) |
| 31 | 12, 30 | eqeltrrd 2842 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ MblFn) |
| 32 | 8 | ismbfcn2 25673 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))) |
| 33 | 32 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶ℂ ∧ (𝑡 ∈ 𝐴 ↦ (𝐹‘𝑡)) ∈ MblFn) → ((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
| 34 | 31, 33 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
| 35 | 34 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) |
| 36 | | ftc1anclem1 37700 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))):𝐴⟶ℝ ∧ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) ∈ MblFn) |
| 37 | 28, 35, 36 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℜ‘(𝐹‘𝑡)))) ∈ MblFn) |
| 38 | 26, 37 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn) |
| 39 | 10, 18, 38 | iblabsnc 37691 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡)))) ∈
𝐿1) |
| 40 | 19 | abscld 15475 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ) |
| 41 | 19 | absge0d 15483 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → 0 ≤
(abs‘(ℜ‘(𝐹‘𝑡)))) |
| 42 | 40, 41 | iblpos 25828 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (abs‘(ℜ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
| 44 | 39, 43 | mpbid 232 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℜ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ)) |
| 45 | 44 | simprd 495 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 46 | 45 | adantr 480 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℜ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 47 | 7, 46 | eqeltrd 2841 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℜ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 48 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝐺 = ℑ → (𝐺‘(𝐹‘𝑡)) = (ℑ‘(𝐹‘𝑡))) |
| 49 | 48 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝐺 = ℑ →
(abs‘(𝐺‘(𝐹‘𝑡))) = (abs‘(ℑ‘(𝐹‘𝑡)))) |
| 50 | 49 | ifeq1d 4545 |
. . . . . . . 8
⊢ (𝐺 = ℑ → if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0) = if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) |
| 51 | 50 | mpteq2dv 5244 |
. . . . . . 7
⊢ (𝐺 = ℑ → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) |
| 52 | 51 | fveq2d 6910 |
. . . . . 6
⊢ (𝐺 = ℑ →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
| 53 | 52 | adantl 481 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℑ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
| 54 | 8 | imcld 15234 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ) |
| 55 | 54 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ) |
| 56 | 55 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝑡 ∈ 𝐴) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ) |
| 57 | 17 | simprd 495 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1) |
| 58 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) = (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) |
| 59 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ℑ‘(𝐹‘𝑡)) → (abs‘𝑥) = (abs‘(ℑ‘(𝐹‘𝑡)))) |
| 60 | 55, 58, 23, 59 | fmptco 7149 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℂ → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡))))) |
| 61 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) = (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡))))) |
| 62 | 54 | fmpttd 7135 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶ℂ → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
| 63 | 62 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))):𝐴⟶ℝ) |
| 64 | 34 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn) |
| 65 | | ftc1anclem1 37700 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))):𝐴⟶ℝ ∧ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) ∈ MblFn) |
| 66 | 63, 64, 65 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (abs
∘ (𝑡 ∈ 𝐴 ↦ (ℑ‘(𝐹‘𝑡)))) ∈ MblFn) |
| 67 | 61, 66 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn) |
| 68 | 56, 57, 67 | iblabsnc 37691 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) → (𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡)))) ∈
𝐿1) |
| 69 | 55 | abscld 15475 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ) |
| 70 | 55 | absge0d 15483 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝑡 ∈ 𝐴) → 0 ≤
(abs‘(ℑ‘(𝐹‘𝑡)))) |
| 71 | 69, 70 | iblpos 25828 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶ℂ → ((𝑡 ∈ 𝐴 ↦ (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
| 72 | 71 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ))) |
| 73 | 68, 72 | mpbid 232 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
((𝑡 ∈ 𝐴 ↦
(abs‘(ℑ‘(𝐹‘𝑡)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ)) |
| 74 | 73 | simprd 495 |
. . . . . 6
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 75 | 74 | adantr 480 |
. . . . 5
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℑ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 76 | 53, 75 | eqeltrd 2841 |
. . . 4
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 = ℑ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 77 | 47, 76 | jaodan 960 |
. . 3
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ (𝐺 = ℜ ∨ 𝐺 = ℑ)) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 78 | 1, 77 | sylan2 593 |
. 2
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1) ∧ 𝐺 ∈ {ℜ, ℑ})
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
| 79 | 78 | 3impa 1110 |
1
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ 𝐺 ∈ {ℜ, ℑ})
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐴, (abs‘(𝐺‘(𝐹‘𝑡))), 0))) ∈ ℝ) |