Metamath Proof Explorer

Theorem itgmulc2lem2

Description: Lemma for itgmulc2 : real case. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 
|- ( ph -> C e. CC )
itgmulc2.2 
|- ( ( ph /\ x e. A ) -> B e. V )
itgmulc2.3 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
itgmulc2.4 
|- ( ph -> C e. RR )
itgmulc2.5 
|- ( ( ph /\ x e. A ) -> B e. RR )
Assertion itgmulc2lem2 
|- ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )

Proof

Step Hyp Ref Expression
1 itgmulc2.1 
 |-  ( ph -> C e. CC )
2 itgmulc2.2 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 itgmulc2.3 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
4 itgmulc2.4 
 |-  ( ph -> C e. RR )
5 itgmulc2.5 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
6 4 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
7 max0sub 
 |-  ( C e. RR -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
8 6 7 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
9 8 oveq1d 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( C x. B ) )
10 0re 
 |-  0 e. RR
11 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
12 4 10 11 sylancl 
 |-  ( ph -> if ( 0 <_ C , C , 0 ) e. RR )
13 12 recnd 
 |-  ( ph -> if ( 0 <_ C , C , 0 ) e. CC )
14 13 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. CC )
15 4 renegcld 
 |-  ( ph -> -u C e. RR )
16 ifcl 
 |-  ( ( -u C e. RR /\ 0 e. RR ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
17 15 10 16 sylancl 
 |-  ( ph -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
18 17 recnd 
 |-  ( ph -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
19 18 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
20 5 recnd 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
21 14 19 20 subdird 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
22 9 21 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
23 22 itgeq2dv 
 |-  ( ph -> S. A ( C x. B ) _d x = S. A ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) _d x )
24 12 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
25 24 5 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. B ) e. RR )
26 13 2 3 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) e. L^1 )
27 17 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
28 27 5 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) e. RR )
29 18 2 3 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) e. L^1 )
30 25 26 28 29 itgsub 
 |-  ( ph -> S. A ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) _d x = ( S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x ) )
31 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
32 5 10 31 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
33 24 32 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. RR )
34 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 ) ) )
35 3 34 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 ) )
36 35 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 )
37 13 32 36 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. L^1 )
38 5 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
39 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
40 38 10 39 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
41 24 40 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. RR )
42 35 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 )
43 13 40 42 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. L^1 )
44 33 37 41 43 itgsub 
 |-  ( ph -> S. A ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x = ( S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
45 max0sub 
 |-  ( B e. RR -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
46 5 45 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
47 46 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( if ( 0 <_ C , C , 0 ) x. B ) )
48 32 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
49 40 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. CC )
50 14 48 49 subdid 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
51 47 50 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
52 51 itgeq2dv 
 |-  ( ph -> S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x = S. A ( ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x )
53 5 3 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 ) )
54 53 oveq2d 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) = ( if ( 0 <_ C , C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
55 32 36 itgcl 
 |-  ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x e. CC )
56 40 42 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x e. CC )
57 13 55 56 subdid 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
58 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
59 10 4 58 sylancr 
 |-  ( ph -> 0 <_ if ( 0 <_ C , C , 0 ) )
60 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
61 10 5 60 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
62 13 32 36 12 32 59 61 itgmulc2lem1 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) = S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x )
63 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
64 10 38 63 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
65 13 40 42 12 40 59 64 itgmulc2lem1 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) = S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x )
66 62 65 oveq12d 
 |-  ( ph -> ( ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ C , C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
67 54 57 66 3eqtrd 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) = ( S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
68 44 52 67 3eqtr4d 
 |-  ( ph -> S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x = ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) )
69 27 32 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. RR )
70 18 32 36 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. L^1 )
71 27 40 remulcld 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. RR )
72 18 40 42 iblmulc2 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. L^1 )
73 69 70 71 72 itgsub 
 |-  ( ph -> S. A ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x = ( S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
74 46 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( if ( 0 <_ -u C , -u C , 0 ) x. B ) )
75 19 48 49 subdid 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) ) = ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
76 74 75 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) = ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
77 76 itgeq2dv 
 |-  ( ph -> S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x = S. A ( ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) - ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) _d x )
78 53 oveq2d 
 |-  ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) = ( if ( 0 <_ -u C , -u C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
79 18 55 56 subdid 
 |-  ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. ( S. A if ( 0 <_ B , B , 0 ) _d x - S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) )
80 max1 
 |-  ( ( 0 e. RR /\ -u C e. RR ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
81 10 15 80 sylancr 
 |-  ( ph -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
82 18 32 36 17 32 81 61 itgmulc2lem1 
 |-  ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) = S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x )
83 18 40 42 17 40 81 64 itgmulc2lem1 
 |-  ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) = S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x )
84 82 83 oveq12d 
 |-  ( ph -> ( ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ B , B , 0 ) _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A if ( 0 <_ -u B , -u B , 0 ) _d x ) ) = ( S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
85 78 79 84 3eqtrd 
 |-  ( ph -> ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) = ( S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) _d x ) )
86 73 77 85 3eqtr4d 
 |-  ( ph -> S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x = ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) )
87 68 86 oveq12d 
 |-  ( ph -> ( S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x ) = ( ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) ) )
88 2 3 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
89 13 18 88 subdird 
 |-  ( ph -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. S. A B _d x ) = ( ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) - ( if ( 0 <_ -u C , -u C , 0 ) x. S. A B _d x ) ) )
90 4 7 syl 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
91 90 oveq1d 
 |-  ( ph -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. S. A B _d x ) = ( C x. S. A B _d x ) )
92 87 89 91 3eqtr2d 
 |-  ( ph -> ( S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x - S. A ( if ( 0 <_ -u C , -u C , 0 ) x. B ) _d x ) = ( C x. S. A B _d x ) )
93 23 30 92 3eqtrrd 
 |-  ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )