Metamath Proof Explorer

Theorem itgneg

Description: Negation of an integral. (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 itgneg 
|- ( ph -> -u S. A B _d x = S. A -u B _d x )

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 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
7 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 ) ) )
8 2 7 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
9 8 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
10 6 9 itgcl 
 |-  ( ph -> S. A ( Re ` B ) _d x e. CC )
11 ax-icn 
 |-  _i e. CC
12 5 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
13 8 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
14 12 13 itgcl 
 |-  ( ph -> S. A ( Im ` B ) _d x e. CC )
15 mulcl 
 |-  ( ( _i e. CC /\ S. A ( Im ` B ) _d x e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
16 11 14 15 sylancr 
 |-  ( ph -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
17 10 16 negdid 
 |-  ( ph -> -u ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) = ( -u S. A ( Re ` B ) _d x + -u ( _i x. S. A ( Im ` B ) _d x ) ) )
18 0re 
 |-  0 e. RR
19 ifcl 
 |-  ( ( ( Re ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) e. RR )
20 6 18 19 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) e. RR )
21 6 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 ) ) )
22 9 21 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 ) )
23 22 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) ) e. L^1 )
24 20 23 itgcl 
 |-  ( ph -> S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x e. CC )
25 6 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` B ) e. RR )
26 ifcl 
 |-  ( ( -u ( Re ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) e. RR )
27 25 18 26 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) e. RR )
28 22 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) ) e. L^1 )
29 27 28 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x e. CC )
30 24 29 negsubdi2d 
 |-  ( ph -> -u ( S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x ) = ( S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x - S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x ) )
31 6 9 itgreval 
 |-  ( ph -> S. A ( Re ` B ) _d x = ( S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x ) )
32 31 negeqd 
 |-  ( ph -> -u S. A ( Re ` B ) _d x = -u ( S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x ) )
33 5 negcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
34 33 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) e. RR )
35 1 2 iblneg 
 |-  ( ph -> ( x e. A |-> -u B ) e. L^1 )
36 33 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 ) ) )
37 35 36 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` -u B ) ) e. L^1 /\ ( x e. A |-> ( Im ` -u B ) ) e. L^1 ) )
38 37 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` -u B ) ) e. L^1 )
39 34 38 itgreval 
 |-  ( ph -> S. A ( Re ` -u B ) _d x = ( S. A if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) _d x ) )
40 5 renegd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) = -u ( Re ` B ) )
41 40 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( Re ` -u B ) <-> 0 <_ -u ( Re ` B ) ) )
42 41 40 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) = if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) )
43 42 itgeq2dv 
 |-  ( ph -> S. A if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) _d x = S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x )
44 40 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` -u B ) = -u -u ( Re ` B ) )
45 6 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
46 45 negnegd 
 |-  ( ( ph /\ x e. A ) -> -u -u ( Re ` B ) = ( Re ` B ) )
47 44 46 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` -u B ) = ( Re ` B ) )
48 47 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u ( Re ` -u B ) <-> 0 <_ ( Re ` B ) ) )
49 48 47 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) = if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) )
50 49 itgeq2dv 
 |-  ( ph -> S. A if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) _d x = S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x )
51 43 50 oveq12d 
 |-  ( ph -> ( S. A if ( 0 <_ ( Re ` -u B ) , ( Re ` -u B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Re ` -u B ) , -u ( Re ` -u B ) , 0 ) _d x ) = ( S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x - S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x ) )
52 39 51 eqtrd 
 |-  ( ph -> S. A ( Re ` -u B ) _d x = ( S. A if ( 0 <_ -u ( Re ` B ) , -u ( Re ` B ) , 0 ) _d x - S. A if ( 0 <_ ( Re ` B ) , ( Re ` B ) , 0 ) _d x ) )
53 30 32 52 3eqtr4d 
 |-  ( ph -> -u S. A ( Re ` B ) _d x = S. A ( Re ` -u B ) _d x )
54 mulneg2 
 |-  ( ( _i e. CC /\ S. A ( Im ` B ) _d x e. CC ) -> ( _i x. -u S. A ( Im ` B ) _d x ) = -u ( _i x. S. A ( Im ` B ) _d x ) )
55 11 14 54 sylancr 
 |-  ( ph -> ( _i x. -u S. A ( Im ` B ) _d x ) = -u ( _i x. S. A ( Im ` B ) _d x ) )
56 ifcl 
 |-  ( ( ( Im ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) e. RR )
57 12 18 56 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) e. RR )
58 12 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 ) ) )
59 13 58 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 ) )
60 59 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) ) e. L^1 )
61 57 60 itgcl 
 |-  ( ph -> S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x e. CC )
62 12 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) e. RR )
63 ifcl 
 |-  ( ( -u ( Im ` B ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) e. RR )
64 62 18 63 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) e. RR )
65 59 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) ) e. L^1 )
66 64 65 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x e. CC )
67 61 66 negsubdi2d 
 |-  ( ph -> -u ( S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x ) = ( S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x - S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x ) )
68 5 imnegd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) = -u ( Im ` B ) )
69 68 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( Im ` -u B ) <-> 0 <_ -u ( Im ` B ) ) )
70 69 68 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) = if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) )
71 70 itgeq2dv 
 |-  ( ph -> S. A if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) _d x = S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x )
72 68 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` -u B ) = -u -u ( Im ` B ) )
73 12 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
74 73 negnegd 
 |-  ( ( ph /\ x e. A ) -> -u -u ( Im ` B ) = ( Im ` B ) )
75 72 74 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` -u B ) = ( Im ` B ) )
76 75 breq2d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ -u ( Im ` -u B ) <-> 0 <_ ( Im ` B ) ) )
77 76 75 ifbieq1d 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) = if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) )
78 77 itgeq2dv 
 |-  ( ph -> S. A if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) _d x = S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x )
79 71 78 oveq12d 
 |-  ( ph -> ( S. A if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) _d x ) = ( S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x - S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x ) )
80 67 79 eqtr4d 
 |-  ( ph -> -u ( S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x ) = ( S. A if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) _d x ) )
81 12 13 itgreval 
 |-  ( ph -> S. A ( Im ` B ) _d x = ( S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x ) )
82 81 negeqd 
 |-  ( ph -> -u S. A ( Im ` B ) _d x = -u ( S. A if ( 0 <_ ( Im ` B ) , ( Im ` B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` B ) , -u ( Im ` B ) , 0 ) _d x ) )
83 33 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) e. RR )
84 37 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` -u B ) ) e. L^1 )
85 83 84 itgreval 
 |-  ( ph -> S. A ( Im ` -u B ) _d x = ( S. A if ( 0 <_ ( Im ` -u B ) , ( Im ` -u B ) , 0 ) _d x - S. A if ( 0 <_ -u ( Im ` -u B ) , -u ( Im ` -u B ) , 0 ) _d x ) )
86 80 82 85 3eqtr4d 
 |-  ( ph -> -u S. A ( Im ` B ) _d x = S. A ( Im ` -u B ) _d x )
87 86 oveq2d 
 |-  ( ph -> ( _i x. -u S. A ( Im ` B ) _d x ) = ( _i x. S. A ( Im ` -u B ) _d x ) )
88 55 87 eqtr3d 
 |-  ( ph -> -u ( _i x. S. A ( Im ` B ) _d x ) = ( _i x. S. A ( Im ` -u B ) _d x ) )
89 53 88 oveq12d 
 |-  ( ph -> ( -u S. A ( Re ` B ) _d x + -u ( _i x. S. A ( Im ` B ) _d x ) ) = ( S. A ( Re ` -u B ) _d x + ( _i x. S. A ( Im ` -u B ) _d x ) ) )
90 17 89 eqtrd 
 |-  ( ph -> -u ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) = ( S. A ( Re ` -u B ) _d x + ( _i x. S. A ( Im ` -u B ) _d x ) ) )
91 1 2 itgcnval 
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
92 91 negeqd 
 |-  ( ph -> -u S. A B _d x = -u ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
93 33 35 itgcnval 
 |-  ( ph -> S. A -u B _d x = ( S. A ( Re ` -u B ) _d x + ( _i x. S. A ( Im ` -u B ) _d x ) ) )
94 90 92 93 3eqtr4d 
 |-  ( ph -> -u S. A B _d x = S. A -u B _d x )