Metamath Proof Explorer

Theorem itgaddlem1

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 )
itgadd.7 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
itgadd.8 
|- ( ( ph /\ x e. A ) -> 0 <_ C )
Assertion itgaddlem1 
|- ( 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 itgadd.7 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
8 itgadd.8 
 |-  ( ( ph /\ x e. A ) -> 0 <_ C )
9 5 6 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
10 1 2 3 4 ibladd 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )
11 5 6 7 8 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( B + C ) )
12 9 10 11 itgposval 
 |-  ( ph -> S. A ( B + C ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) ) ) )
13 5 2 7 itgposval 
 |-  ( ph -> S. A B _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
14 6 4 8 itgposval 
 |-  ( ph -> S. A C _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) )
15 13 14 oveq12d 
 |-  ( ph -> ( S. A B _d x + S. A C _d x ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) ) )
16 5 7 iblpos 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) ) )
17 2 16 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )
18 17 simpld 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
19 18 5 mbfdm2 
 |-  ( ph -> A e. dom vol )
20 mblss 
 |-  ( A e. dom vol -> A C_ RR )
21 19 20 syl 
 |-  ( ph -> A C_ RR )
22 rembl 
 |-  RR e. dom vol
23 22 a1i 
 |-  ( ph -> RR e. dom vol )
24 elrege0 
 |-  ( B e. ( 0 [,) +oo ) <-> ( B e. RR /\ 0 <_ B ) )
25 5 7 24 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
26 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
27 26 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,) +oo ) )
28 25 27 ifclda 
 |-  ( ph -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
29 28 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
30 eldifn 
 |-  ( x e. ( RR \ A ) -> -. x e. A )
31 30 adantl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> -. x e. A )
32 31 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , B , 0 ) = 0 )
33 iftrue 
 |-  ( x e. A -> if ( x e. A , B , 0 ) = B )
34 33 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , B , 0 ) ) = ( x e. A |-> B )
35 34 18 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , B , 0 ) ) e. MblFn )
36 21 23 29 32 35 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) e. MblFn )
37 28 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
38 37 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
39 17 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
40 elrege0 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
41 6 8 40 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> C e. ( 0 [,) +oo ) )
42 41 27 ifclda 
 |-  ( ph -> if ( x e. A , C , 0 ) e. ( 0 [,) +oo ) )
43 42 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( x e. A , C , 0 ) e. ( 0 [,) +oo ) )
44 31 iffalsed 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , C , 0 ) = 0 )
45 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
46 45 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , C , 0 ) ) = ( x e. A |-> C )
47 6 8 iblpos 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> C ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) e. RR ) ) )
48 4 47 mpbid 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) e. RR ) )
49 48 simpld 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
50 46 49 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , C , 0 ) ) e. MblFn )
51 21 23 43 44 50 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , C , 0 ) ) e. MblFn )
52 42 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,) +oo ) )
53 52 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , C , 0 ) ) : RR --> ( 0 [,) +oo ) )
54 48 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) e. RR )
55 36 38 39 51 53 54 itg2add 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( x e. A , B , 0 ) ) oF + ( x e. RR |-> if ( x e. A , C , 0 ) ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) ) )
56 reex 
 |-  RR e. _V
57 56 a1i 
 |-  ( ph -> RR e. _V )
58 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
59 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , C , 0 ) ) = ( x e. RR |-> if ( x e. A , C , 0 ) ) )
60 57 37 52 58 59 offval2 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , B , 0 ) ) oF + ( x e. RR |-> if ( x e. A , C , 0 ) ) ) = ( x e. RR |-> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) ) )
61 33 45 oveq12d 
 |-  ( x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = ( B + C ) )
62 iftrue 
 |-  ( x e. A -> if ( x e. A , ( B + C ) , 0 ) = ( B + C ) )
63 61 62 eqtr4d 
 |-  ( x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = if ( x e. A , ( B + C ) , 0 ) )
64 iffalse 
 |-  ( -. x e. A -> if ( x e. A , B , 0 ) = 0 )
65 iffalse 
 |-  ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
66 64 65 oveq12d 
 |-  ( -. x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = ( 0 + 0 ) )
67 00id 
 |-  ( 0 + 0 ) = 0
68 66 67 eqtrdi 
 |-  ( -. x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = 0 )
69 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( B + C ) , 0 ) = 0 )
70 68 69 eqtr4d 
 |-  ( -. x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = if ( x e. A , ( B + C ) , 0 ) )
71 63 70 pm2.61i 
 |-  ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = if ( x e. A , ( B + C ) , 0 )
72 71 mpteq2i 
 |-  ( x e. RR |-> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) )
73 60 72 eqtrdi 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , B , 0 ) ) oF + ( x e. RR |-> if ( x e. A , C , 0 ) ) ) = ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) ) )
74 73 fveq2d 
 |-  ( ph -> ( S.2 ` ( ( x e. RR |-> if ( x e. A , B , 0 ) ) oF + ( x e. RR |-> if ( x e. A , C , 0 ) ) ) ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) ) ) )
75 15 55 74 3eqtr2d 
 |-  ( ph -> ( S. A B _d x + S. A C _d x ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) ) ) )
76 12 75 eqtr4d 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )