Metamath Proof Explorer

Theorem ibladd

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 ibladd 
|- ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )

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 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
6 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
7 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
8 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
9 5 6 7 8 1 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) ) )
10 2 9 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) )
11 10 simp1d 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
12 11 1 mbfdm2 
 |-  ( ph -> A e. dom vol )
13 eqidd 
 |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
14 eqidd 
 |-  ( ph -> ( x e. A |-> C ) = ( x e. A |-> C ) )
15 12 1 3 13 14 offval2 
 |-  ( ph -> ( ( x e. A |-> B ) oF + ( x e. A |-> C ) ) = ( x e. A |-> ( B + C ) ) )
16 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) )
17 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) )
18 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) )
19 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) )
20 16 17 18 19 3 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> C ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR ) ) ) )
21 4 20 mpbid 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR ) ) )
22 21 simp1d 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
23 11 22 mbfadd 
 |-  ( ph -> ( ( x e. A |-> B ) oF + ( x e. A |-> C ) ) e. MblFn )
24 15 23 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
25 11 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
26 25 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
27 22 3 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
28 27 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. RR )
29 25 27 readdd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B + C ) ) = ( ( Re ` B ) + ( Re ` C ) ) )
30 25 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )
31 11 30 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) )
32 31 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. MblFn )
33 27 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn <-> ( ( x e. A |-> ( Re ` C ) ) e. MblFn /\ ( x e. A |-> ( Im ` C ) ) e. MblFn ) ) )
34 22 33 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` C ) ) e. MblFn /\ ( x e. A |-> ( Im ` C ) ) e. MblFn ) )
35 34 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` C ) ) e. MblFn )
36 10 simp2d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) )
37 36 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR )
38 21 simp2d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR ) )
39 38 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR )
40 26 28 29 32 35 37 39 ibladdlem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) e. RR )
41 26 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` B ) e. RR )
42 28 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` C ) e. RR )
43 29 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` ( B + C ) ) = -u ( ( Re ` B ) + ( Re ` C ) ) )
44 26 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
45 28 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. CC )
46 44 45 negdid 
 |-  ( ( ph /\ x e. A ) -> -u ( ( Re ` B ) + ( Re ` C ) ) = ( -u ( Re ` B ) + -u ( Re ` C ) ) )
47 43 46 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` ( B + C ) ) = ( -u ( Re ` B ) + -u ( Re ` C ) ) )
48 26 32 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( Re ` B ) ) e. MblFn )
49 28 35 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( Re ` C ) ) e. MblFn )
50 36 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR )
51 38 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR )
52 41 42 47 48 49 50 51 ibladdlem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) e. RR )
53 40 52 jca 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) e. RR ) )
54 25 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
55 27 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. RR )
56 25 27 imaddd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( B + C ) ) = ( ( Im ` B ) + ( Im ` C ) ) )
57 31 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. MblFn )
58 34 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` C ) ) e. MblFn )
59 10 simp3d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) )
60 59 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR )
61 21 simp3d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR ) )
62 61 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR )
63 54 55 56 57 58 60 62 ibladdlem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) e. RR )
64 54 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) e. RR )
65 55 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` C ) e. RR )
66 56 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` ( B + C ) ) = -u ( ( Im ` B ) + ( Im ` C ) ) )
67 54 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
68 55 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. CC )
69 67 68 negdid 
 |-  ( ( ph /\ x e. A ) -> -u ( ( Im ` B ) + ( Im ` C ) ) = ( -u ( Im ` B ) + -u ( Im ` C ) ) )
70 66 69 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` ( B + C ) ) = ( -u ( Im ` B ) + -u ( Im ` C ) ) )
71 54 57 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( Im ` B ) ) e. MblFn )
72 55 58 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( Im ` C ) ) e. MblFn )
73 59 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR )
74 61 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR )
75 64 65 70 71 72 73 74 ibladdlem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) e. RR )
76 63 75 jca 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) e. RR ) )
77 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) )
78 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) )
79 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) )
80 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) )
81 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. _V )
82 77 78 79 80 81 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) e. L^1 <-> ( ( x e. A |-> ( B + C ) ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) e. RR ) ) ) )
83 24 53 76 82 mpbir3and 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )