Metamath Proof Explorer

Theorem iblneg

Description: The negative of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 
|- ( ( ph /\ x e. A ) -> B e. V )
itgcnval.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion iblneg 
|- ( ph -> ( x e. A |-> -u B ) e. L^1 )

Proof

Step Hyp Ref Expression
1 itgcnval.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgcnval.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
4 2 3 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
5 4 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 5 renegd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) = -u ( Re ` B ) )
7 6 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( Re ` -u B ) <-> 0 <_ -u ( Re ` B ) ) )
8 7 6 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) = if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) )
9 8 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) ) )
10 5 iblcn 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) )
11 2 10 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
12 11 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
13 5 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
14 13 iblre 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) ) e. L^1 ) ) )
15 12 14 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) ) e. L^1 ) )
16 15 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) ) e. L^1 )
17 9 16 eqeltrd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) ) e. L^1 )
18 6 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` -u B ) = -u -u ( Re ` B ) )
19 13 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
20 19 negnegd 
 |-  ( ( ph /\ x e. A ) -> -u -u ( Re ` B ) = ( Re ` B ) )
21 18 20 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` -u B ) = ( Re ` B ) )
22 21 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u ( Re ` -u B ) <-> 0 <_ ( Re ` B ) ) )
23 22 21 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) = if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) ) = ( x e. A |-> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) ) )
25 15 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) ) e. L^1 )
26 24 25 eqeltrd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) ) e. L^1 )
27 5 negcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
28 27 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) e. RR )
29 28 iblre 
 |-  ( ph -> ( ( x e. A |-> ( Re ` -u B ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) ) e. L^1 ) ) )
30 17 26 29 mpbir2and 
 |-  ( ph -> ( x e. A |-> ( Re ` -u B ) ) e. L^1 )
31 5 imnegd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) = -u ( Im ` B ) )
32 31 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( Im ` -u B ) <-> 0 <_ -u ( Im ` B ) ) )
33 32 31 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) = if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) )
34 33 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) ) = ( x e. A |-> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) ) )
35 11 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
36 5 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
37 36 iblre 
 |-  ( ph -> ( ( x e. A |-> ( Im ` B ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) ) e. L^1 ) ) )
38 35 37 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) ) e. L^1 ) )
39 38 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) ) e. L^1 )
40 34 39 eqeltrd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) ) e. L^1 )
41 31 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` -u B ) = -u -u ( Im ` B ) )
42 36 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
43 42 negnegd 
 |-  ( ( ph /\ x e. A ) -> -u -u ( Im ` B ) = ( Im ` B ) )
44 41 43 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` -u B ) = ( Im ` B ) )
45 44 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u ( Im ` -u B ) <-> 0 <_ ( Im ` B ) ) )
46 45 44 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) = if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) )
47 46 mpteq2dva 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) ) = ( x e. A |-> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) ) )
48 38 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) ) e. L^1 )
49 47 48 eqeltrd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) ) e. L^1 )
50 27 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) e. RR )
51 50 iblre 
 |-  ( ph -> ( ( x e. A |-> ( Im ` -u B ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) ) e. L^1 ) ) )
52 40 49 51 mpbir2and 
 |-  ( ph -> ( x e. A |-> ( Im ` -u B ) ) e. L^1 )
53 27 iblcn 
 |-  ( ph -> ( ( x e. A |-> -u B ) e. L^1 <-> ( ( x e. A |-> ( Re ` -u B ) ) e. L^1 /\ ( x e. A |-> ( Im ` -u B ) ) e. L^1 ) ) )
54 30 52 53 mpbir2and 
 |-  ( ph -> ( x e. A |-> -u B ) e. L^1 )