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 ) |