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 --> CC /\ F e. L^1 /\ G e. { Re , Im } ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( G e. { Re , Im } -> ( G = Re \/ G = Im ) )
2 fveq1 
 |-  ( G = Re -> ( G ` ( F ` t ) ) = ( Re ` ( F ` t ) ) )
3 2 fveq2d 
 |-  ( G = Re -> ( abs ` ( G ` ( F ` t ) ) ) = ( abs ` ( Re ` ( F ` t ) ) ) )
4 3 ifeq1d 
 |-  ( G = Re -> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) = if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) )
5 4 mpteq2dv 
 |-  ( G = Re -> ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) = ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) )
6 5 fveq2d 
 |-  ( G = Re -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) )
7 6 adantl 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G = Re ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) )
8 ffvelcdm 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( F ` t ) e. CC )
9 8 recld 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( Re ` ( F ` t ) ) e. RR )
10 9 adantlr 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ t e. A ) -> ( Re ` ( F ` t ) ) e. RR )
11 simpl 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> F : A --> CC )
12 11 feqmptd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> F = ( t e. A |-> ( F ` t ) ) )
13 simpr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> F e. L^1 )
14 12 13 eqeltrrd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( F ` t ) ) e. L^1 )
15 8 iblcn 
 |-  ( F : A --> CC -> ( ( t e. A |-> ( F ` t ) ) e. L^1 <-> ( ( t e. A |-> ( Re ` ( F ` t ) ) ) e. L^1 /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. L^1 ) ) )
16 15 biimpa 
 |-  ( ( F : A --> CC /\ ( t e. A |-> ( F ` t ) ) e. L^1 ) -> ( ( t e. A |-> ( Re ` ( F ` t ) ) ) e. L^1 /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. L^1 ) )
17 14 16 syldan 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( ( t e. A |-> ( Re ` ( F ` t ) ) ) e. L^1 /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. L^1 ) )
18 17 simpld 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( Re ` ( F ` t ) ) ) e. L^1 )
19 9 recnd 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( Re ` ( F ` t ) ) e. CC )
20 eqidd 
 |-  ( F : A --> CC -> ( t e. A |-> ( Re ` ( F ` t ) ) ) = ( t e. A |-> ( Re ` ( F ` t ) ) ) )
21 absf 
 |-  abs : CC --> RR
22 21 a1i 
 |-  ( F : A --> CC -> abs : CC --> RR )
23 22 feqmptd 
 |-  ( F : A --> CC -> abs = ( x e. CC |-> ( abs ` x ) ) )
24 fveq2 
 |-  ( x = ( Re ` ( F ` t ) ) -> ( abs ` x ) = ( abs ` ( Re ` ( F ` t ) ) ) )
25 19 20 23 24 fmptco 
 |-  ( F : A --> CC -> ( abs o. ( t e. A |-> ( Re ` ( F ` t ) ) ) ) = ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) )
26 25 adantr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( abs o. ( t e. A |-> ( Re ` ( F ` t ) ) ) ) = ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) )
27 9 fmpttd 
 |-  ( F : A --> CC -> ( t e. A |-> ( Re ` ( F ` t ) ) ) : A --> RR )
28 27 adantr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( Re ` ( F ` t ) ) ) : A --> RR )
29 iblmbf 
 |-  ( F e. L^1 -> F e. MblFn )
30 29 adantl 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> F e. MblFn )
31 12 30 eqeltrrd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( F ` t ) ) e. MblFn )
32 8 ismbfcn2 
 |-  ( F : A --> CC -> ( ( t e. A |-> ( F ` t ) ) e. MblFn <-> ( ( t e. A |-> ( Re ` ( F ` t ) ) ) e. MblFn /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. MblFn ) ) )
33 32 biimpa 
 |-  ( ( F : A --> CC /\ ( t e. A |-> ( F ` t ) ) e. MblFn ) -> ( ( t e. A |-> ( Re ` ( F ` t ) ) ) e. MblFn /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. MblFn ) )
34 31 33 syldan 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( ( t e. A |-> ( Re ` ( F ` t ) ) ) e. MblFn /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. MblFn ) )
35 34 simpld 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( Re ` ( F ` t ) ) ) e. MblFn )
36 ftc1anclem1 
 |-  ( ( ( t e. A |-> ( Re ` ( F ` t ) ) ) : A --> RR /\ ( t e. A |-> ( Re ` ( F ` t ) ) ) e. MblFn ) -> ( abs o. ( t e. A |-> ( Re ` ( F ` t ) ) ) ) e. MblFn )
37 28 35 36 syl2anc 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( abs o. ( t e. A |-> ( Re ` ( F ` t ) ) ) ) e. MblFn )
38 26 37 eqeltrrd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. MblFn )
39 10 18 38 iblabsnc 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. L^1 )
40 19 abscld 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( abs ` ( Re ` ( F ` t ) ) ) e. RR )
41 19 absge0d 
 |-  ( ( F : A --> CC /\ t e. A ) -> 0 <_ ( abs ` ( Re ` ( F ` t ) ) ) )
42 40 41 iblpos 
 |-  ( F : A --> CC -> ( ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. L^1 <-> ( ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) e. RR ) ) )
43 42 adantr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. L^1 <-> ( ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) e. RR ) ) )
44 39 43 mpbid 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( ( t e. A |-> ( abs ` ( Re ` ( F ` t ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) e. RR ) )
45 44 simprd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
46 45 adantr 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G = Re ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Re ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
47 7 46 eqeltrd 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G = Re ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
48 fveq1 
 |-  ( G = Im -> ( G ` ( F ` t ) ) = ( Im ` ( F ` t ) ) )
49 48 fveq2d 
 |-  ( G = Im -> ( abs ` ( G ` ( F ` t ) ) ) = ( abs ` ( Im ` ( F ` t ) ) ) )
50 49 ifeq1d 
 |-  ( G = Im -> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) = if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) )
51 50 mpteq2dv 
 |-  ( G = Im -> ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) = ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) )
52 51 fveq2d 
 |-  ( G = Im -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) )
53 52 adantl 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G = Im ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) = ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) )
54 8 imcld 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( Im ` ( F ` t ) ) e. RR )
55 54 recnd 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( Im ` ( F ` t ) ) e. CC )
56 55 adantlr 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ t e. A ) -> ( Im ` ( F ` t ) ) e. CC )
57 17 simprd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( Im ` ( F ` t ) ) ) e. L^1 )
58 eqidd 
 |-  ( F : A --> CC -> ( t e. A |-> ( Im ` ( F ` t ) ) ) = ( t e. A |-> ( Im ` ( F ` t ) ) ) )
59 fveq2 
 |-  ( x = ( Im ` ( F ` t ) ) -> ( abs ` x ) = ( abs ` ( Im ` ( F ` t ) ) ) )
60 55 58 23 59 fmptco 
 |-  ( F : A --> CC -> ( abs o. ( t e. A |-> ( Im ` ( F ` t ) ) ) ) = ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) )
61 60 adantr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( abs o. ( t e. A |-> ( Im ` ( F ` t ) ) ) ) = ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) )
62 54 fmpttd 
 |-  ( F : A --> CC -> ( t e. A |-> ( Im ` ( F ` t ) ) ) : A --> RR )
63 62 adantr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( Im ` ( F ` t ) ) ) : A --> RR )
64 34 simprd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( Im ` ( F ` t ) ) ) e. MblFn )
65 ftc1anclem1 
 |-  ( ( ( t e. A |-> ( Im ` ( F ` t ) ) ) : A --> RR /\ ( t e. A |-> ( Im ` ( F ` t ) ) ) e. MblFn ) -> ( abs o. ( t e. A |-> ( Im ` ( F ` t ) ) ) ) e. MblFn )
66 63 64 65 syl2anc 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( abs o. ( t e. A |-> ( Im ` ( F ` t ) ) ) ) e. MblFn )
67 61 66 eqeltrrd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. MblFn )
68 56 57 67 iblabsnc 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. L^1 )
69 55 abscld 
 |-  ( ( F : A --> CC /\ t e. A ) -> ( abs ` ( Im ` ( F ` t ) ) ) e. RR )
70 55 absge0d 
 |-  ( ( F : A --> CC /\ t e. A ) -> 0 <_ ( abs ` ( Im ` ( F ` t ) ) ) )
71 69 70 iblpos 
 |-  ( F : A --> CC -> ( ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. L^1 <-> ( ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) e. RR ) ) )
72 71 adantr 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. L^1 <-> ( ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) e. RR ) ) )
73 68 72 mpbid 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( ( t e. A |-> ( abs ` ( Im ` ( F ` t ) ) ) ) e. MblFn /\ ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) e. RR ) )
74 73 simprd 
 |-  ( ( F : A --> CC /\ F e. L^1 ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
75 74 adantr 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G = Im ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( Im ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
76 53 75 eqeltrd 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G = Im ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
77 47 76 jaodan 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ ( G = Re \/ G = Im ) ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
78 1 77 sylan2 
 |-  ( ( ( F : A --> CC /\ F e. L^1 ) /\ G e. { Re , Im } ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) e. RR )
79 78 3impa 
 |-  ( ( F : A --> CC /\ F e. L^1 /\ G e. { Re , Im } ) -> ( S.2 ` ( t e. RR |-> if ( t e. A , ( abs ` ( G ` ( F ` t ) ) ) , 0 ) ) ) e. RR )