Metamath Proof Explorer

Theorem itgcnval

Description: Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-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 itgcnval 
|- ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` 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 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
4 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
5 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
6 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
7 3 4 5 6 1 2 itgcnlem 
 |-  ( ph -> S. A B _d x = ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) ) + ( _i x. ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) ) ) ) )
8 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
9 2 8 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
10 9 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
11 10 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
12 10 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 ) ) )
13 2 12 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
14 13 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
15 11 14 itgrevallem1 
 |-  ( ph -> S. A ( Re ` B ) _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) ) )
16 10 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
17 13 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
18 16 17 itgrevallem1 
 |-  ( ph -> S. A ( Im ` B ) _d x = ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) ) )
19 18 oveq2d 
 |-  ( ph -> ( _i x. S. A ( Im ` B ) _d x ) = ( _i x. ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) ) ) )
20 15 19 oveq12d 
 |-  ( ph -> ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) = ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) ) + ( _i x. ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) - ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) ) ) ) )
21 7 20 eqtr4d 
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )