Metamath Proof Explorer

Theorem itgaddnclem1

Description: Lemma for itgaddnc ; cf. itgaddlem1 . (Contributed by Brendan Leahy, 7-Nov-2017)

Ref Expression
Hypotheses ibladdnc.1 
|- ( ( ph /\ x e. A ) -> B e. V )
ibladdnc.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
ibladdnc.3 
|- ( ( ph /\ x e. A ) -> C e. V )
ibladdnc.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
ibladdnc.m 
|- ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
itgaddnclem.1 
|- ( ( ph /\ x e. A ) -> B e. RR )
itgaddnclem.2 
|- ( ( ph /\ x e. A ) -> C e. RR )
itgaddnclem.3 
|- ( ( ph /\ x e. A ) -> 0 <_ B )
itgaddnclem.4 
|- ( ( ph /\ x e. A ) -> 0 <_ C )
Assertion itgaddnclem1 
|- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )

Proof

Step Hyp Ref Expression
1 ibladdnc.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 ibladdnc.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 ibladdnc.3 
 |-  ( ( ph /\ x e. A ) -> C e. V )
4 ibladdnc.4 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
5 ibladdnc.m 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
6 itgaddnclem.1 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
7 itgaddnclem.2 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
8 itgaddnclem.3 
 |-  ( ( ph /\ x e. A ) -> 0 <_ B )
9 itgaddnclem.4 
 |-  ( ( ph /\ x e. A ) -> 0 <_ C )
10 6 7 readdcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. RR )
11 1 2 3 4 5 ibladdnc 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )
12 6 7 8 9 addge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( B + C ) )
13 10 11 12 itgposval 
 |-  ( ph -> S. A ( B + C ) _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) ) ) )
14 6 2 8 itgposval 
 |-  ( ph -> S. A B _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) )
15 7 4 9 itgposval 
 |-  ( ph -> S. A C _d x = ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) )
16 14 15 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 ) ) ) ) )
17 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
18 2 17 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
19 18 1 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 6 8 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 iffalse 
 |-  ( -. x e. A -> if ( x e. A , B , 0 ) = 0 )
33 31 32 syl 
 |-  ( ( ph /\ x e. ( RR \ A ) ) -> if ( x e. A , B , 0 ) = 0 )
34 iftrue 
 |-  ( x e. A -> if ( x e. A , B , 0 ) = B )
35 34 mpteq2ia 
 |-  ( x e. A |-> if ( x e. A , B , 0 ) ) = ( x e. A |-> B )
36 35 18 eqeltrid 
 |-  ( ph -> ( x e. A |-> if ( x e. A , B , 0 ) ) e. MblFn )
37 21 23 29 33 36 mbfss 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) e. MblFn )
38 28 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , B , 0 ) e. ( 0 [,) +oo ) )
39 38 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) : RR --> ( 0 [,) +oo ) )
40 6 8 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 ) ) )
41 2 40 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR ) )
42 41 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , B , 0 ) ) ) e. RR )
43 elrege0 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
44 7 9 43 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> C e. ( 0 [,) +oo ) )
45 44 27 ifclda 
 |-  ( ph -> if ( x e. A , C , 0 ) e. ( 0 [,) +oo ) )
46 45 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,) +oo ) )
47 46 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , C , 0 ) ) : RR --> ( 0 [,) +oo ) )
48 7 9 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 ) ) )
49 4 48 mpbid 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) e. RR ) )
50 49 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , C , 0 ) ) ) e. RR )
51 37 39 42 47 50 itg2addnc 
 |-  ( 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 ) ) ) ) )
52 reex 
 |-  RR e. _V
53 52 a1i 
 |-  ( ph -> RR e. _V )
54 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , B , 0 ) ) = ( x e. RR |-> if ( x e. A , B , 0 ) ) )
55 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , C , 0 ) ) = ( x e. RR |-> if ( x e. A , C , 0 ) ) )
56 53 38 46 54 55 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 ) ) ) )
57 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
58 34 57 oveq12d 
 |-  ( x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = ( B + C ) )
59 iftrue 
 |-  ( x e. A -> if ( x e. A , ( B + C ) , 0 ) = ( B + C ) )
60 58 59 eqtr4d 
 |-  ( x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = if ( x e. A , ( B + C ) , 0 ) )
61 iffalse 
 |-  ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
62 32 61 oveq12d 
 |-  ( -. x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = ( 0 + 0 ) )
63 00id 
 |-  ( 0 + 0 ) = 0
64 62 63 eqtrdi 
 |-  ( -. x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = 0 )
65 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( B + C ) , 0 ) = 0 )
66 64 65 eqtr4d 
 |-  ( -. x e. A -> ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = if ( x e. A , ( B + C ) , 0 ) )
67 60 66 pm2.61i 
 |-  ( if ( x e. A , B , 0 ) + if ( x e. A , C , 0 ) ) = if ( x e. A , ( B + C ) , 0 )
68 67 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 ) )
69 56 68 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 ) ) )
70 69 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 ) ) ) )
71 16 51 70 3eqtr2d 
 |-  ( ph -> ( S. A B _d x + S. A C _d x ) = ( S.2 ` ( x e. RR |-> if ( x e. A , ( B + C ) , 0 ) ) ) )
72 13 71 eqtr4d 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )