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∈ℝ⟼ift∈AG⁡F⁡t0∈ℝ

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=ℜ→ift∈AG⁡F⁡t0=ift∈Aℜ⁡F⁡t0
5 4 mpteq2dv ⊢G=ℜ→t∈ℝ⟼ift∈AG⁡F⁡t0=t∈ℝ⟼ift∈Aℜ⁡F⁡t0
6 5 fveq2d ⊢G=ℜ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0=∫2⁡t∈ℝ⟼ift∈Aℜ⁡F⁡t0
7 6 adantl ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℜ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0=∫2⁡t∈ℝ⟼ift∈Aℜ⁡F⁡t0
8 ffvelcdm ⊢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∈ℝ⟼ift∈Aℜ⁡F⁡t0∈ℝ
43 42 adantr ⊢F:A⟶ℂ∧F∈𝐿1→t∈A⟼ℜ⁡F⁡t∈𝐿1↔t∈A⟼ℜ⁡F⁡t∈MblFn∧∫2⁡t∈ℝ⟼ift∈Aℜ⁡F⁡t0∈ℝ
44 39 43 mpbid ⊢F:A⟶ℂ∧F∈𝐿1→t∈A⟼ℜ⁡F⁡t∈MblFn∧∫2⁡t∈ℝ⟼ift∈Aℜ⁡F⁡t0∈ℝ
45 44 simprd ⊢F:A⟶ℂ∧F∈𝐿1→∫2⁡t∈ℝ⟼ift∈Aℜ⁡F⁡t0∈ℝ
46 45 adantr ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℜ→∫2⁡t∈ℝ⟼ift∈Aℜ⁡F⁡t0∈ℝ
47 7 46 eqeltrd ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℜ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0∈ℝ
48 fveq1 ⊢G=ℑ→G⁡F⁡t=ℑ⁡F⁡t
49 48 fveq2d ⊢G=ℑ→G⁡F⁡t=ℑ⁡F⁡t
50 49 ifeq1d ⊢G=ℑ→ift∈AG⁡F⁡t0=ift∈Aℑ⁡F⁡t0
51 50 mpteq2dv ⊢G=ℑ→t∈ℝ⟼ift∈AG⁡F⁡t0=t∈ℝ⟼ift∈Aℑ⁡F⁡t0
52 51 fveq2d ⊢G=ℑ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0=∫2⁡t∈ℝ⟼ift∈Aℑ⁡F⁡t0
53 52 adantl ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℑ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0=∫2⁡t∈ℝ⟼ift∈Aℑ⁡F⁡t0
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∈ℝ⟼ift∈Aℑ⁡F⁡t0∈ℝ
72 71 adantr ⊢F:A⟶ℂ∧F∈𝐿1→t∈A⟼ℑ⁡F⁡t∈𝐿1↔t∈A⟼ℑ⁡F⁡t∈MblFn∧∫2⁡t∈ℝ⟼ift∈Aℑ⁡F⁡t0∈ℝ
73 68 72 mpbid ⊢F:A⟶ℂ∧F∈𝐿1→t∈A⟼ℑ⁡F⁡t∈MblFn∧∫2⁡t∈ℝ⟼ift∈Aℑ⁡F⁡t0∈ℝ
74 73 simprd ⊢F:A⟶ℂ∧F∈𝐿1→∫2⁡t∈ℝ⟼ift∈Aℑ⁡F⁡t0∈ℝ
75 74 adantr ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℑ→∫2⁡t∈ℝ⟼ift∈Aℑ⁡F⁡t0∈ℝ
76 53 75 eqeltrd ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℑ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0∈ℝ
77 47 76 jaodan ⊢F:A⟶ℂ∧F∈𝐿1∧G=ℜ∨G=ℑ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0∈ℝ
78 1 77 sylan2 ⊢F:A⟶ℂ∧F∈𝐿1∧G∈ℜℑ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0∈ℝ
79 78 3impa ⊢F:A⟶ℂ∧F∈𝐿1∧G∈ℜℑ→∫2⁡t∈ℝ⟼ift∈AG⁡F⁡t0∈ℝ