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