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