Metamath Proof Explorer

Theorem itgmulc2nclem2

Description: Lemma for itgmulc2nc ; cf. itgmulc2lem2 . (Contributed by Brendan Leahy, 19-Nov-2017)

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

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 
 |-  ( ph -> C e. CC )
2 itgmulc2nc.2 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 itgmulc2nc.3 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
4 itgmulc2nc.m 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )
5 itgmulc2nc.4 
 |-  ( ph -> C e. RR )
6 itgmulc2nc.5 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
7 max0sub 
 |-  ( C e. RR -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
8 5 7 syl 
 |-  ( ph -> ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) = C )
9 8 oveq1d 
 |-  ( ph -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( C x. B ) )
10 9 adantr 
 |-  ( ( ph /\ x e. A ) -> ( ( if ( 0 <_ C , C , 0 ) - if ( 0 <_ -u C , -u C , 0 ) ) x. B ) = ( C x. B ) )
11 0re 
 |-  0 e. RR
12 ifcl 
 |-  ( ( C e. RR /\ 0 e. RR ) -> if ( 0 <_ C , C , 0 ) e. RR )
13 5 11 12 sylancl 
 |-  ( ph -> if ( 0 <_ C , C , 0 ) e. RR )
14 13 recnd 
 |-  ( ph -> if ( 0 <_ C , C , 0 ) e. CC )
15 14 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. CC )
16 5 renegcld 
 |-  ( ph -> -u C e. RR )
17 ifcl 
 |-  ( ( -u C e. RR /\ 0 e. RR ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
18 16 11 17 sylancl 
 |-  ( ph -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
19 18 recnd 
 |-  ( ph -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
20 19 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. CC )
21 6 recnd 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
22 15 20 21 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 ) ) )
23 10 22 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) = ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
24 23 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 )
25 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. B ) e. _V )
26 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) e. _V )
27 4 26 mbfdm2 
 |-  ( ph -> A e. dom vol )
28 13 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ C , C , 0 ) e. RR )
29 fconstmpt 
 |-  ( A X. { if ( 0 <_ C , C , 0 ) } ) = ( x e. A |-> if ( 0 <_ C , C , 0 ) )
30 29 a1i 
 |-  ( ph -> ( A X. { if ( 0 <_ C , C , 0 ) } ) = ( x e. A |-> if ( 0 <_ C , C , 0 ) ) )
31 eqidd 
 |-  ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
32 27 28 6 30 31 offval2 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) )
33 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
34 3 33 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
35 21 fmpttd 
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
36 34 13 35 mbfmulc2re 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> B ) ) e. MblFn )
37 32 36 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) e. MblFn )
38 14 6 3 37 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) e. L^1 )
39 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) e. _V )
40 18 adantr 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u C , -u C , 0 ) e. RR )
41 fconstmpt 
 |-  ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) = ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) )
42 41 a1i 
 |-  ( ph -> ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) = ( x e. A |-> if ( 0 <_ -u C , -u C , 0 ) ) )
43 27 40 6 42 31 offval2 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) )
44 34 18 35 mbfmulc2re 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> B ) ) e. MblFn )
45 43 44 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) e. MblFn )
46 19 6 3 45 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) e. L^1 )
47 23 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) = ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) ) )
48 47 4 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( if ( 0 <_ C , C , 0 ) x. B ) - ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) ) e. MblFn )
49 25 38 39 46 48 itgsubnc 
 |-  ( 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 ) )
50 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. _V )
51 ifcl 
 |-  ( ( B e. RR /\ 0 e. RR ) -> if ( 0 <_ B , B , 0 ) e. RR )
52 6 11 51 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. RR )
53 6 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 ) ) )
54 3 53 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 ) )
55 54 simpld 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. L^1 )
56 eqidd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) = ( x e. A |-> if ( 0 <_ B , B , 0 ) ) )
57 27 28 52 30 56 offval2 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) )
58 6 34 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) e. MblFn )
59 52 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ B , B , 0 ) e. CC )
60 59 fmpttd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ B , B , 0 ) ) : A --> CC )
61 58 13 60 mbfmulc2re 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
62 57 61 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
63 14 52 55 62 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. L^1 )
64 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. _V )
65 6 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
66 ifcl 
 |-  ( ( -u B e. RR /\ 0 e. RR ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
67 65 11 66 sylancl 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. RR )
68 54 simprd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. L^1 )
69 eqidd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) = ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) )
70 27 28 67 30 69 offval2 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
71 6 34 mbfneg 
 |-  ( ph -> ( x e. A |-> -u B ) e. MblFn )
72 65 71 mbfpos 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) e. MblFn )
73 67 recnd 
 |-  ( ( ph /\ x e. A ) -> if ( 0 <_ -u B , -u B , 0 ) e. CC )
74 73 fmpttd 
 |-  ( ph -> ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) : A --> CC )
75 72 13 74 mbfmulc2re 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
76 70 75 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
77 14 67 68 76 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. L^1 )
78 max0sub 
 |-  ( B e. RR -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
79 6 78 syl 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ B , B , 0 ) - if ( 0 <_ -u B , -u B , 0 ) ) = B )
80 79 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 ) )
81 15 59 73 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 ) ) ) )
82 80 81 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 ) ) ) )
83 82 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ C , C , 0 ) x. B ) ) = ( x e. 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 ) ) ) ) )
84 32 83 eqtrd 
 |-  ( ph -> ( ( A X. { if ( 0 <_ C , C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. 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 ) ) ) ) )
85 84 36 eqeltrrd 
 |-  ( ph -> ( x e. 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 ) ) ) ) e. MblFn )
86 50 63 64 77 85 itgsubnc 
 |-  ( 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 ) )
87 82 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 )
88 6 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 ) )
89 88 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 ) ) )
90 52 55 itgcl 
 |-  ( ph -> S. A if ( 0 <_ B , B , 0 ) _d x e. CC )
91 67 68 itgcl 
 |-  ( ph -> S. A if ( 0 <_ -u B , -u B , 0 ) _d x e. CC )
92 14 90 91 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 ) ) )
93 max1 
 |-  ( ( 0 e. RR /\ C e. RR ) -> 0 <_ if ( 0 <_ C , C , 0 ) )
94 11 5 93 sylancr 
 |-  ( ph -> 0 <_ if ( 0 <_ C , C , 0 ) )
95 max1 
 |-  ( ( 0 e. RR /\ B e. RR ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
96 11 6 95 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ B , B , 0 ) )
97 14 52 55 62 13 52 94 96 itgmulc2nclem1 
 |-  ( 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 )
98 max1 
 |-  ( ( 0 e. RR /\ -u B e. RR ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
99 11 65 98 sylancr 
 |-  ( ( ph /\ x e. A ) -> 0 <_ if ( 0 <_ -u B , -u B , 0 ) )
100 14 67 68 76 13 67 94 99 itgmulc2nclem1 
 |-  ( 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 )
101 97 100 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 ) )
102 89 92 101 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 ) )
103 86 87 102 3eqtr4d 
 |-  ( ph -> S. A ( if ( 0 <_ C , C , 0 ) x. B ) _d x = ( if ( 0 <_ C , C , 0 ) x. S. A B _d x ) )
104 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) e. _V )
105 27 40 52 42 56 offval2 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) )
106 58 18 60 mbfmulc2re 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
107 105 106 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. MblFn )
108 19 52 55 107 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ B , B , 0 ) ) ) e. L^1 )
109 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) e. _V )
110 27 40 67 42 69 offval2 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) = ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) )
111 72 18 74 mbfmulc2re 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
112 110 111 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. MblFn )
113 19 67 68 112 iblmulc2nc 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. if ( 0 <_ -u B , -u B , 0 ) ) ) e. L^1 )
114 79 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 ) )
115 20 59 73 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 ) ) ) )
116 114 115 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 ) ) ) )
117 116 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( if ( 0 <_ -u C , -u C , 0 ) x. B ) ) = ( x e. 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 ) ) ) ) )
118 43 117 eqtrd 
 |-  ( ph -> ( ( A X. { if ( 0 <_ -u C , -u C , 0 ) } ) oF x. ( x e. A |-> B ) ) = ( x e. 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 ) ) ) ) )
119 118 44 eqeltrrd 
 |-  ( ph -> ( x e. 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 ) ) ) ) e. MblFn )
120 104 108 109 113 119 itgsubnc 
 |-  ( 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 ) )
121 116 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 )
122 88 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 ) ) )
123 19 90 91 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 ) ) )
124 max1 
 |-  ( ( 0 e. RR /\ -u C e. RR ) -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
125 11 16 124 sylancr 
 |-  ( ph -> 0 <_ if ( 0 <_ -u C , -u C , 0 ) )
126 19 52 55 107 18 52 125 96 itgmulc2nclem1 
 |-  ( 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 )
127 19 67 68 112 18 67 125 99 itgmulc2nclem1 
 |-  ( 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 )
128 126 127 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 ) )
129 122 123 128 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 ) )
130 120 121 129 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 ) )
131 103 130 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 ) ) )
132 6 3 itgcl 
 |-  ( ph -> S. A B _d x e. CC )
133 14 19 132 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 ) ) )
134 8 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 ) )
135 131 133 134 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 ) )
136 24 49 135 3eqtrrd 
 |-  ( ph -> ( C x. S. A B _d x ) = S. A ( C x. B ) _d x )