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 ffvelrn
 |-  ( ( 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 )