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 ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐹 ∈ 𝐿1 ∧ 𝐺 ∈ { ℜ , ℑ } ) → ( ∫2 ‘ ( 𝑡 ∈ ℝ ↦ if ( 𝑡 ∈ 𝐴 , ( abs ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑡 ) ) ) , 0 ) ) ) ∈ ℝ )

Proof

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