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 )