Metamath Proof Explorer

Theorem ftc1anclem2

Description: Lemma for ftc1anc - restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018) (Revised by Brendan Leahy, 8-Aug-2018)

Ref Expression
Assertion ftc1anclem2 ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G ∈ ℜ ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 ∈ ℝ

Proof

Step Hyp Ref Expression
1 elpri ⊢ G ∈ ℜ ℑ → G = ℜ ∨ G = ℑ
2 fveq1 ⊢ G = ℜ → G ⁡ F ⁡ t = ℜ ⁡ F ⁡ t
3 2 fveq2d ⊢ G = ℜ → G ⁡ F ⁡ t = ℜ ⁡ F ⁡ t
4 3 ifeq1d ⊢ G = ℜ → if t ∈ A G ⁡ F ⁡ t 0 = if t ∈ A ℜ ⁡ F ⁡ t 0
5 4 mpteq2dv ⊢ G = ℜ → t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 = t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0
6 5 fveq2d ⊢ G = ℜ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 = ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0
7 6 adantl ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℜ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 = ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0
8 ffvelrn ⊢ F : A ⟶ ℂ ∧ t ∈ A → F ⁡ t ∈ ℂ
9 8 recld ⊢ F : A ⟶ ℂ ∧ t ∈ A → ℜ ⁡ F ⁡ t ∈ ℝ
10 9 adantlr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ t ∈ A → ℜ ⁡ F ⁡ t ∈ ℝ
11 simpl ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → F : A ⟶ ℂ
12 11 feqmptd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → F = t ∈ A ⟼ F ⁡ t
13 simpr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → F ∈ 𝐿 1
14 12 13 eqeltrrd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ F ⁡ t ∈ 𝐿 1
15 8 iblcn ⊢ F : A ⟶ ℂ → t ∈ A ⟼ F ⁡ t ∈ 𝐿 1 ↔ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1 ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1
16 15 biimpa ⊢ F : A ⟶ ℂ ∧ t ∈ A ⟼ F ⁡ t ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1 ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1
17 14 16 syldan ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1 ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1
18 17 simpld ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1
19 9 recnd ⊢ F : A ⟶ ℂ ∧ t ∈ A → ℜ ⁡ F ⁡ t ∈ ℂ
20 eqidd ⊢ F : A ⟶ ℂ → t ∈ A ⟼ ℜ ⁡ F ⁡ t = t ∈ A ⟼ ℜ ⁡ F ⁡ t
21 absf ⊢ abs : ℂ ⟶ ℝ
22 21 a1i ⊢ F : A ⟶ ℂ → abs : ℂ ⟶ ℝ
23 22 feqmptd ⊢ F : A ⟶ ℂ → abs = x ∈ ℂ ⟼ x
24 fveq2 ⊢ x = ℜ ⁡ F ⁡ t → x = ℜ ⁡ F ⁡ t
25 19 20 23 24 fmptco ⊢ F : A ⟶ ℂ → abs ∘ t ∈ A ⟼ ℜ ⁡ F ⁡ t = t ∈ A ⟼ ℜ ⁡ F ⁡ t
26 25 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → abs ∘ t ∈ A ⟼ ℜ ⁡ F ⁡ t = t ∈ A ⟼ ℜ ⁡ F ⁡ t
27 9 fmpttd ⊢ F : A ⟶ ℂ → t ∈ A ⟼ ℜ ⁡ F ⁡ t : A ⟶ ℝ
28 27 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t : A ⟶ ℝ
29 iblmbf ⊢ F ∈ 𝐿 1 → F ∈ MblFn
30 29 adantl ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → F ∈ MblFn
31 12 30 eqeltrrd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ F ⁡ t ∈ MblFn
32 8 ismbfcn2 ⊢ F : A ⟶ ℂ → t ∈ A ⟼ F ⁡ t ∈ MblFn ↔ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
33 32 biimpa ⊢ F : A ⟶ ℂ ∧ t ∈ A ⟼ F ⁡ t ∈ MblFn → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
34 31 33 syldan ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
35 34 simpld ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn
36 ftc1anclem1 ⊢ t ∈ A ⟼ ℜ ⁡ F ⁡ t : A ⟶ ℝ ∧ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn → abs ∘ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn
37 28 35 36 syl2anc ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → abs ∘ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn
38 26 37 eqeltrrd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn
39 10 18 38 iblabsnc ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1
40 19 abscld ⊢ F : A ⟶ ℂ ∧ t ∈ A → ℜ ⁡ F ⁡ t ∈ ℝ
41 19 absge0d ⊢ F : A ⟶ ℂ ∧ t ∈ A → 0 ≤ ℜ ⁡ F ⁡ t
42 40 41 iblpos ⊢ F : A ⟶ ℂ → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1 ↔ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn ∧ ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0 ∈ ℝ
43 42 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ 𝐿 1 ↔ t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn ∧ ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0 ∈ ℝ
44 39 43 mpbid ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℜ ⁡ F ⁡ t ∈ MblFn ∧ ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0 ∈ ℝ
45 44 simprd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0 ∈ ℝ
46 45 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℜ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℜ ⁡ F ⁡ t 0 ∈ ℝ
47 7 46 eqeltrd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℜ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 ∈ ℝ
48 fveq1 ⊢ G = ℑ → G ⁡ F ⁡ t = ℑ ⁡ F ⁡ t
49 48 fveq2d ⊢ G = ℑ → G ⁡ F ⁡ t = ℑ ⁡ F ⁡ t
50 49 ifeq1d ⊢ G = ℑ → if t ∈ A G ⁡ F ⁡ t 0 = if t ∈ A ℑ ⁡ F ⁡ t 0
51 50 mpteq2dv ⊢ G = ℑ → t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 = t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0
52 51 fveq2d ⊢ G = ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 = ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0
53 52 adantl ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 = ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0
54 8 imcld ⊢ F : A ⟶ ℂ ∧ t ∈ A → ℑ ⁡ F ⁡ t ∈ ℝ
55 54 recnd ⊢ F : A ⟶ ℂ ∧ t ∈ A → ℑ ⁡ F ⁡ t ∈ ℂ
56 55 adantlr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ t ∈ A → ℑ ⁡ F ⁡ t ∈ ℂ
57 17 simprd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1
58 eqidd ⊢ F : A ⟶ ℂ → t ∈ A ⟼ ℑ ⁡ F ⁡ t = t ∈ A ⟼ ℑ ⁡ F ⁡ t
59 fveq2 ⊢ x = ℑ ⁡ F ⁡ t → x = ℑ ⁡ F ⁡ t
60 55 58 23 59 fmptco ⊢ F : A ⟶ ℂ → abs ∘ t ∈ A ⟼ ℑ ⁡ F ⁡ t = t ∈ A ⟼ ℑ ⁡ F ⁡ t
61 60 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → abs ∘ t ∈ A ⟼ ℑ ⁡ F ⁡ t = t ∈ A ⟼ ℑ ⁡ F ⁡ t
62 54 fmpttd ⊢ F : A ⟶ ℂ → t ∈ A ⟼ ℑ ⁡ F ⁡ t : A ⟶ ℝ
63 62 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t : A ⟶ ℝ
64 34 simprd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
65 ftc1anclem1 ⊢ t ∈ A ⟼ ℑ ⁡ F ⁡ t : A ⟶ ℝ ∧ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn → abs ∘ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
66 63 64 65 syl2anc ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → abs ∘ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
67 61 66 eqeltrrd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn
68 56 57 67 iblabsnc ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1
69 55 abscld ⊢ F : A ⟶ ℂ ∧ t ∈ A → ℑ ⁡ F ⁡ t ∈ ℝ
70 55 absge0d ⊢ F : A ⟶ ℂ ∧ t ∈ A → 0 ≤ ℑ ⁡ F ⁡ t
71 69 70 iblpos ⊢ F : A ⟶ ℂ → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1 ↔ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn ∧ ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0 ∈ ℝ
72 71 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ 𝐿 1 ↔ t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn ∧ ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0 ∈ ℝ
73 68 72 mpbid ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → t ∈ A ⟼ ℑ ⁡ F ⁡ t ∈ MblFn ∧ ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0 ∈ ℝ
74 73 simprd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0 ∈ ℝ
75 74 adantr ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A ℑ ⁡ F ⁡ t 0 ∈ ℝ
76 53 75 eqeltrd ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 ∈ ℝ
77 47 76 jaodan ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G = ℜ ∨ G = ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 ∈ ℝ
78 1 77 sylan2 ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G ∈ ℜ ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 ∈ ℝ
79 78 3impa ⊢ F : A ⟶ ℂ ∧ F ∈ 𝐿 1 ∧ G ∈ ℜ ℑ → ∫ 2 ⁡ t ∈ ℝ ⟼ if t ∈ A G ⁡ F ⁡ t 0 ∈ ℝ