This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgim

Description: Imaginary part of an integral. (Contributed by Mario Carneiro, 14-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 itgim 
|- ( ph -> ( Im ` S. A B _d 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 1 2 itgcnval 
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
4 3 fveq2d 
 |-  ( ph -> ( Im ` S. A B _d x ) = ( Im ` ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) )
5 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
6 2 5 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
7 6 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
8 7 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
9 7 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 ) ) )
10 2 9 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
11 10 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
12 8 11 itgrecl 
 |-  ( ph -> S. A ( Re ` B ) _d x e. RR )
13 7 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
14 10 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
15 13 14 itgrecl 
 |-  ( ph -> S. A ( Im ` B ) _d x e. RR )
16 12 15 crimd 
 |-  ( ph -> ( Im ` ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) = S. A ( Im ` B ) _d x )
17 4 16 eqtrd 
 |-  ( ph -> ( Im ` S. A B _d x ) = S. A ( Im ` B ) _d x )