Metamath Proof Explorer

Theorem itgaddlem2

Description: Lemma for itgadd . (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 )
itgadd.5 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgadd.6 
|- ( ( ph /\ x e. A ) -> C e. RR )
Assertion itgaddlem2 
|- ( 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 itgadd.5 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
6 itgadd.6 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
7 max0sub 
 |-  ( B e. RR -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
8 5 7 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
9 max0sub 
 |-  ( C e. RR -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
10 6 9 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
11 8 10 oveq12d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) + ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) ) = ( B + C ) )
12 0re 
 |-  0 e. RR
13 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
14 5 12 13 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
15 14 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
16 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
17 6 12 16 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
18 17 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. CC )
19 5 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
20 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
21 19 12 20 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
22 21 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. CC )
23 6 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u C e. RR )
24 ifcl 
 |-  ( ( -u C e. RR /\ 0 e. RR ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
25 23 12 24 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
26 25 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
27 15 18 22 26 addsub4d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) - ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) = ( ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) + ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) ) )
28 5 6 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
29 max0sub 
 |-  ( ( B + C ) e. RR -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( B + C ) )
30 28 29 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( B + C ) )
31 11 27 30 3eqtr4rd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) - ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) )
32 28 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( B + C ) e. RR )
33 ifcl 
 |-  ( ( -u ( B + C ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) e. RR )
34 32 12 33 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) e. RR )
35 34 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) e. CC )
36 15 18 addcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. CC )
37 ifcl 
 |-  ( ( ( B + C ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) e. RR )
38 28 12 37 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) e. RR )
39 38 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) e. CC )
40 22 26 addcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) e. CC )
41 35 36 39 40 addsubeq4d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) <-> ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) - if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) = ( ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) - ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) ) )
42 31 41 mpbird 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) = ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) )
43 42 itgeq2dv 
 |-  ( ph -> S. A ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) _d x = S. A ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) _d x )
44 1 2 3 4 ibladd 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )
45 28 iblre 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) e. L^1 ) ) )
46 44 45 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) e. L^1 ) )
47 46 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) ) e. L^1 )
48 14 17 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) e. RR )
49 5 iblre 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) ) )
50 2 49 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 ) )
51 50 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 )
52 6 iblre 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) e. L^1 ) ) )
53 4 52 mpbid 
 |-  ( ph -> ( ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. L^1 /\ ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) e. L^1 ) )
54 53 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ C , C , 0 ) ) e. L^1 )
55 14 51 17 54 ibladd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) e. L^1 )
56 max1 
 |-  ( ( 0 e. RR /\ -u ( B + C ) e. RR ) -> 0 <_ if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) )
57 12 32 56 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) )
58 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
59 12 5 58 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
60 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
61 12 6 60 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
62 14 17 59 61 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) )
63 34 47 48 55 34 48 57 62 itgaddlem1 
 |-  ( ph -> S. A ( if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) + ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) ) _d x = ( S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x ) )
64 46 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) ) e. L^1 )
65 21 25 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) e. RR )
66 50 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 )
67 53 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) e. L^1 )
68 21 66 25 67 ibladd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) e. L^1 )
69 max1 
 |-  ( ( 0 e. RR /\ ( B + C ) e. RR ) -> 0 <_ if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) )
70 12 28 69 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) )
71 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
72 12 19 71 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
73 max1 
 |-  ( ( 0 e. RR /\ -u C e. RR ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
74 12 23 73 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
75 21 25 72 74 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) )
76 38 64 65 68 38 65 70 75 itgaddlem1 
 |-  ( ph -> S. A ( if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) + ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) ) _d x = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) )
77 43 63 76 3eqtr3d 
 |-  ( ph -> ( S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x ) = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) )
78 34 47 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x e. CC )
79 14 51 17 54 14 17 59 61 itgaddlem1 
 |-  ( ph -> S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) )
80 14 51 itgcl 
 |-  ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x e. CC )
81 17 54 itgcl 
 |-  ( ph -> S. A if ( 0 <_ C , C , 0 ) _d x e. CC )
82 80 81 addcld 
 |-  ( ph -> ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) e. CC )
83 79 82 eqeltrd 
 |-  ( ph -> S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x e. CC )
84 38 64 itgcl 
 |-  ( ph -> S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x e. CC )
85 21 66 25 67 21 25 72 74 itgaddlem1 
 |-  ( ph -> S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x = ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) )
86 21 66 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x e. CC )
87 25 67 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u C , -u C , 0 ) _d x e. CC )
88 86 87 addcld 
 |-  ( ph -> ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) e. CC )
89 85 88 eqeltrd 
 |-  ( ph -> S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x e. CC )
90 78 83 84 89 addsubeq4d 
 |-  ( ph -> ( ( S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x ) = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x + S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) <-> ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) = ( S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x - S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) ) )
91 77 90 mpbid 
 |-  ( ph -> ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) = ( S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x - S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) )
92 79 85 oveq12d 
 |-  ( ph -> ( S. A ( if ( 0 <_ B , B , 0 ) + if ( 0 <_ C , C , 0 ) ) _d x - S. A ( if ( 0 <_ -u B , -u B , 0 ) + if ( 0 <_ -u C , -u C , 0 ) ) _d x ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) - ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
93 80 81 86 87 addsub4d 
 |-  ( ph -> ( ( S. A if ( 0 <_ B , B , 0 ) _d x + S. A if ( 0 <_ C , C , 0 ) _d x ) - ( S. A if ( 0 <_ -u B , -u B , 0 ) _d x + S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) + ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
94 91 92 93 3eqtrd 
 |-  ( ph -> ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) + ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
95 28 44 itgreval 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A if ( 0 <_ ( B + C ) , ( B + C ) , 0 ) _d x - S. A if ( 0 <_ -u ( B + C ) , -u ( B + C ) , 0 ) _d x ) )
96 5 2 itgreval 
 |-  ( ph -> S. A B _d x = ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) )
97 6 4 itgreval 
 |-  ( ph -> S. A C _d x = ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) )
98 96 97 oveq12d 
 |-  ( ph -> ( S. A B _d x + S. A C _d x ) = ( ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) + ( S. A if ( 0 <_ C , C , 0 ) _d x - S. A if ( 0 <_ -u C , -u C , 0 ) _d x ) ) )
99 94 95 98 3eqtr4d 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )