Step |
Hyp |
Ref |
Expression |
1 |
|
itgadd.1 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
2 |
|
itgadd.2 |
|- ( ph -> ( x e. A |-> B ) e. L^1 ) |
3 |
|
itgadd.3 |
|- ( ( ph /\ x e. A ) -> C e. V ) |
4 |
|
itgadd.4 |
|- ( ph -> ( x e. A |-> C ) e. L^1 ) |
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 |
|
iblmbf |
|- ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn ) |
9 |
4 8
|
syl |
|- ( ph -> ( x e. A |-> C ) e. MblFn ) |
10 |
9 3
|
mbfmptcl |
|- ( ( ph /\ x e. A ) -> C e. CC ) |
11 |
7 10
|
readdd |
|- ( ( ph /\ x e. A ) -> ( Re ` ( B + C ) ) = ( ( Re ` B ) + ( Re ` C ) ) ) |
12 |
11
|
itgeq2dv |
|- ( ph -> S. A ( Re ` ( B + C ) ) _d x = S. A ( ( Re ` B ) + ( Re ` C ) ) _d x ) |
13 |
7
|
recld |
|- ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR ) |
14 |
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 ) ) ) |
15 |
2 14
|
mpbid |
|- ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) |
16 |
15
|
simpld |
|- ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 ) |
17 |
10
|
recld |
|- ( ( ph /\ x e. A ) -> ( Re ` C ) e. RR ) |
18 |
10
|
iblcn |
|- ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> ( Re ` C ) ) e. L^1 /\ ( x e. A |-> ( Im ` C ) ) e. L^1 ) ) ) |
19 |
4 18
|
mpbid |
|- ( ph -> ( ( x e. A |-> ( Re ` C ) ) e. L^1 /\ ( x e. A |-> ( Im ` C ) ) e. L^1 ) ) |
20 |
19
|
simpld |
|- ( ph -> ( x e. A |-> ( Re ` C ) ) e. L^1 ) |
21 |
13 16 17 20 13 17
|
itgaddlem2 |
|- ( ph -> S. A ( ( Re ` B ) + ( Re ` C ) ) _d x = ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) ) |
22 |
12 21
|
eqtrd |
|- ( ph -> S. A ( Re ` ( B + C ) ) _d x = ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) ) |
23 |
7 10
|
imaddd |
|- ( ( ph /\ x e. A ) -> ( Im ` ( B + C ) ) = ( ( Im ` B ) + ( Im ` C ) ) ) |
24 |
23
|
itgeq2dv |
|- ( ph -> S. A ( Im ` ( B + C ) ) _d x = S. A ( ( Im ` B ) + ( Im ` C ) ) _d x ) |
25 |
7
|
imcld |
|- ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR ) |
26 |
15
|
simprd |
|- ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 ) |
27 |
10
|
imcld |
|- ( ( ph /\ x e. A ) -> ( Im ` C ) e. RR ) |
28 |
19
|
simprd |
|- ( ph -> ( x e. A |-> ( Im ` C ) ) e. L^1 ) |
29 |
25 26 27 28 25 27
|
itgaddlem2 |
|- ( ph -> S. A ( ( Im ` B ) + ( Im ` C ) ) _d x = ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) ) |
30 |
24 29
|
eqtrd |
|- ( ph -> S. A ( Im ` ( B + C ) ) _d x = ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) ) |
31 |
30
|
oveq2d |
|- ( ph -> ( _i x. S. A ( Im ` ( B + C ) ) _d x ) = ( _i x. ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) ) ) |
32 |
|
ax-icn |
|- _i e. CC |
33 |
32
|
a1i |
|- ( ph -> _i e. CC ) |
34 |
25 26
|
itgcl |
|- ( ph -> S. A ( Im ` B ) _d x e. CC ) |
35 |
27 28
|
itgcl |
|- ( ph -> S. A ( Im ` C ) _d x e. CC ) |
36 |
33 34 35
|
adddid |
|- ( ph -> ( _i x. ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) ) = ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) ) |
37 |
31 36
|
eqtrd |
|- ( ph -> ( _i x. S. A ( Im ` ( B + C ) ) _d x ) = ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) ) |
38 |
22 37
|
oveq12d |
|- ( ph -> ( S. A ( Re ` ( B + C ) ) _d x + ( _i x. S. A ( Im ` ( B + C ) ) _d x ) ) = ( ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) + ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) ) ) |
39 |
13 16
|
itgcl |
|- ( ph -> S. A ( Re ` B ) _d x e. CC ) |
40 |
17 20
|
itgcl |
|- ( ph -> S. A ( Re ` C ) _d x e. CC ) |
41 |
|
mulcl |
|- ( ( _i e. CC /\ S. A ( Im ` B ) _d x e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) e. CC ) |
42 |
32 34 41
|
sylancr |
|- ( ph -> ( _i x. S. A ( Im ` B ) _d x ) e. CC ) |
43 |
|
mulcl |
|- ( ( _i e. CC /\ S. A ( Im ` C ) _d x e. CC ) -> ( _i x. S. A ( Im ` C ) _d x ) e. CC ) |
44 |
32 35 43
|
sylancr |
|- ( ph -> ( _i x. S. A ( Im ` C ) _d x ) e. CC ) |
45 |
39 40 42 44
|
add4d |
|- ( ph -> ( ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) + ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) ) = ( ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) + ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) ) |
46 |
38 45
|
eqtrd |
|- ( ph -> ( S. A ( Re ` ( B + C ) ) _d x + ( _i x. S. A ( Im ` ( B + C ) ) _d x ) ) = ( ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) + ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) ) |
47 |
|
ovexd |
|- ( ( ph /\ x e. A ) -> ( B + C ) e. _V ) |
48 |
1 2 3 4
|
ibladd |
|- ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 ) |
49 |
47 48
|
itgcnval |
|- ( ph -> S. A ( B + C ) _d x = ( S. A ( Re ` ( B + C ) ) _d x + ( _i x. S. A ( Im ` ( B + C ) ) _d x ) ) ) |
50 |
1 2
|
itgcnval |
|- ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) ) |
51 |
3 4
|
itgcnval |
|- ( ph -> S. A C _d x = ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) |
52 |
50 51
|
oveq12d |
|- ( ph -> ( S. A B _d x + S. A C _d x ) = ( ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) + ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) ) |
53 |
46 49 52
|
3eqtr4d |
|- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) ) |