Metamath Proof Explorer

Theorem itgadd

Description: Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itgadd.1 
|- ( ( ph /\ x e. A ) -> B e. V )
itgadd.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgadd.3 
|- ( ( ph /\ x e. A ) -> C e. V )
itgadd.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
Assertion itgadd 
|- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )

Proof

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