Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  itgaddnclem2 Unicode version

Theorem itgaddnclem2 25499
Description: Lemma for itgaddnc 25500; cf. itgaddlem2 19276. (Contributed by Brendan Leahy, 10-Nov-2017.)
Hypotheses
Ref Expression
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 )
Assertion
Ref Expression
itgaddnclem2  |-  ( ph  ->  S. A ( B  +  C )  _d x  =  ( S. A B  _d x  +  S. A C  _d x ) )
Distinct variable groups:    x, A    x, V    ph, x
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem itgaddnclem2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 itgaddnclem.1 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  B  e.  RR )
2 max0sub 10612 . . . . . . . . . 10  |-  ( B  e.  RR  ->  ( if ( 0  <_  B ,  B ,  0 )  -  if ( 0  <_  -u B ,  -u B ,  0 ) )  =  B )
31, 2syl 15 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  B ,  B ,  0 )  -  if ( 0  <_  -u B ,  -u B ,  0 ) )  =  B )
4 itgaddnclem.2 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  RR )
5 max0sub 10612 . . . . . . . . . 10  |-  ( C  e.  RR  ->  ( if ( 0  <_  C ,  C ,  0 )  -  if ( 0  <_  -u C ,  -u C ,  0 ) )  =  C )
64, 5syl 15 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  C ,  C ,  0 )  -  if ( 0  <_  -u C ,  -u C ,  0 ) )  =  C )
73, 6oveq12d 5960 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
( if ( 0  <_  B ,  B ,  0 )  -  if ( 0  <_  -u B ,  -u B ,  0 ) )  +  ( if ( 0  <_  C ,  C , 
0 )  -  if ( 0  <_  -u C ,  -u C ,  0 ) ) )  =  ( B  +  C
) )
8 0re 8925 . . . . . . . . . . 11  |-  0  e.  RR
9 ifcl 3677 . . . . . . . . . . 11  |-  ( ( B  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_  B ,  B , 
0 )  e.  RR )
101, 8, 9sylancl 643 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  B ,  B ,  0 )  e.  RR )
1110recnd 8948 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  B ,  B ,  0 )  e.  CC )
12 ifcl 3677 . . . . . . . . . . 11  |-  ( ( C  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_  C ,  C , 
0 )  e.  RR )
134, 8, 12sylancl 643 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  C ,  C ,  0 )  e.  RR )
1413recnd 8948 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  C ,  C ,  0 )  e.  CC )
151renegcld 9297 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  -u B  e.  RR )
16 ifcl 3677 . . . . . . . . . . 11  |-  ( (
-u B  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_  -u B ,  -u B ,  0 )  e.  RR )
1715, 8, 16sylancl 643 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  -u B ,  -u B ,  0 )  e.  RR )
1817recnd 8948 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  -u B ,  -u B ,  0 )  e.  CC )
194renegcld 9297 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  -u C  e.  RR )
20 ifcl 3677 . . . . . . . . . . 11  |-  ( (
-u C  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_  -u C ,  -u C ,  0 )  e.  RR )
2119, 8, 20sylancl 643 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  -u C ,  -u C ,  0 )  e.  RR )
2221recnd 8948 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  -u C ,  -u C ,  0 )  e.  CC )
2311, 14, 18, 22addsub4d 9291 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) )  -  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) ) )  =  ( ( if ( 0  <_  B ,  B , 
0 )  -  if ( 0  <_  -u B ,  -u B ,  0 ) )  +  ( if ( 0  <_  C ,  C , 
0 )  -  if ( 0  <_  -u C ,  -u C ,  0 ) ) ) )
241, 4readdcld 8949 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( B  +  C )  e.  RR )
25 max0sub 10612 . . . . . . . . 9  |-  ( ( B  +  C )  e.  RR  ->  ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  -  if ( 0  <_  -u ( B  +  C ) , 
-u ( B  +  C ) ,  0 ) )  =  ( B  +  C ) )
2624, 25syl 15 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  -  if ( 0  <_  -u ( B  +  C ) , 
-u ( B  +  C ) ,  0 ) )  =  ( B  +  C ) )
277, 23, 263eqtr4rd 2401 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  -  if ( 0  <_  -u ( B  +  C ) , 
-u ( B  +  C ) ,  0 ) )  =  ( ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) )  -  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) ) ) )
2824renegcld 9297 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  -u ( B  +  C )  e.  RR )
29 ifcl 3677 . . . . . . . . . 10  |-  ( (
-u ( B  +  C )  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C
) ,  0 )  e.  RR )
3028, 8, 29sylancl 643 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C ) ,  0 )  e.  RR )
3130recnd 8948 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C ) ,  0 )  e.  CC )
3210, 13readdcld 8949 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) )  e.  RR )
3332recnd 8948 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) )  e.  CC )
34 ifcl 3677 . . . . . . . . . 10  |-  ( ( ( B  +  C
)  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_ 
( B  +  C
) ,  ( B  +  C ) ,  0 )  e.  RR )
3524, 8, 34sylancl 643 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  e.  RR )
3635recnd 8948 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  e.  CC )
3717, 21readdcld 8949 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) )  e.  RR )
3837recnd 8948 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) )  e.  CC )
3931, 33, 36, 38addsubeq4d 9295 . . . . . . 7  |-  ( (
ph  /\  x  e.  A )  ->  (
( if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C
) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  =  ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  +  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) ) )  <->  ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  -  if ( 0  <_  -u ( B  +  C ) , 
-u ( B  +  C ) ,  0 ) )  =  ( ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) )  -  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) ) ) ) )
4027, 39mpbird 223 . . . . . 6  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C ) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  =  ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  +  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) ) ) )
4140itgeq2dv 19234 . . . . 5  |-  ( ph  ->  S. A ( if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C ) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  _d x  =  S. A ( if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 )  +  ( if ( 0  <_  -u B ,  -u B ,  0 )  +  if ( 0  <_  -u C ,  -u C ,  0 ) ) )  _d x )
42 ibladdnc.2 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )
43 ibladdnc.4 . . . . . . . . 9  |-  ( ph  ->  ( x  e.  A  |->  C )  e.  L ^1 )
44 ibladdnc.m . . . . . . . . 9  |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C
) )  e. MblFn )
451, 42, 4, 43, 44ibladdnc 25497 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  ( B  +  C
) )  e.  L ^1 )
4624iblre 19246 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  A  |->  ( B  +  C ) )  e.  L ^1  <->  ( (
x  e.  A  |->  if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 ) )  e.  L ^1  /\  ( x  e.  A  |->  if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C
) ,  0 ) )  e.  L ^1 ) ) )
4745, 46mpbid 201 . . . . . . 7  |-  ( ph  ->  ( ( x  e.  A  |->  if ( 0  <_  ( B  +  C ) ,  ( B  +  C ) ,  0 ) )  e.  L ^1  /\  ( x  e.  A  |->  if ( 0  <_  -u ( B  +  C
) ,  -u ( B  +  C ) ,  0 ) )  e.  L ^1 ) )
4847simprd 449 . . . . . 6  |-  ( ph  ->  ( x  e.  A  |->  if ( 0  <_  -u ( B  +  C
) ,  -u ( B  +  C ) ,  0 ) )  e.  L ^1 )
491iblre 19246 . . . . . . . . 9  |-  ( 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 ) ) )
5042, 49mpbid 201 . . . . . . . 8  |-  ( 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 ) )
5150simpld 445 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  |->  if ( 0  <_  B ,  B , 
0 ) )  e.  L ^1 )
524iblre 19246 . . . . . . . . 9  |-  ( ph  ->  ( ( x  e.  A  |->  C )  e.  L ^1  <->  ( (
x  e.  A  |->  if ( 0  <_  C ,  C ,  0 ) )  e.  L ^1 
/\  ( x  e.  A  |->  if ( 0  <_  -u C ,  -u C ,  0 ) )  e.  L ^1 ) ) )
5343, 52mpbid 201 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  A  |->  if ( 0  <_  C ,  C ,  0 ) )  e.  L ^1  /\  ( x  e.  A  |->  if ( 0  <_  -u C ,  -u C ,  0 ) )  e.  L ^1 ) )
5453simpld 445 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  |->  if ( 0  <_  C ,  C , 
0 ) )  e.  L ^1 )
55 eqid 2358 . . . . . . . . 9  |-  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  =  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )
5632, 55fmptd 5764 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) ) : A --> RR )
57 iftrue 3647 . . . . . . . . . . . . . . 15  |-  ( [ y  /  x ]
0  <_  C  ->  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 )  =  [_ y  /  x ]_ C )
5857oveq2d 5958 . . . . . . . . . . . . . 14  |-  ( [ y  /  x ]
0  <_  C  ->  (
[_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  [_ y  /  x ]_ C ) )
5958adantl 452 . . . . . . . . . . . . 13  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  C )  ->  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  [_ y  /  x ]_ C ) )
60 ovex 5967 . . . . . . . . . . . . . . 15  |-  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )  e.  _V
61 nfcv 2494 . . . . . . . . . . . . . . . 16  |-  F/_ x
y
62 nfcsb1v 3189 . . . . . . . . . . . . . . . . 17  |-  F/_ x [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )
63 nfcv 2494 . . . . . . . . . . . . . . . . 17  |-  F/_ x  +
64 nfs1v 2111 . . . . . . . . . . . . . . . . . 18  |-  F/ x [ y  /  x ] 0  <_  C
65 nfcsb1v 3189 . . . . . . . . . . . . . . . . . 18  |-  F/_ x [_ y  /  x ]_ C
66 nfcv 2494 . . . . . . . . . . . . . . . . . 18  |-  F/_ x
0
6764, 65, 66nfif 3665 . . . . . . . . . . . . . . . . 17  |-  F/_ x if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 )
6862, 63, 67nfov 5965 . . . . . . . . . . . . . . . 16  |-  F/_ x
( [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )
69 csbeq1a 3165 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  if ( 0  <_  B ,  B ,  0 )  =  [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 ) )
70 sbequ12 1924 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
0  <_  C  <->  [ y  /  x ] 0  <_  C ) )
71 csbeq1a 3165 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  C  =  [_ y  /  x ]_ C )
72 eqidd 2359 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  0  =  0 )
7370, 71, 72ifbieq12d 3663 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  if ( 0  <_  C ,  C ,  0 )  =  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )
7469, 73oveq12d 5960 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) ) )
7561, 68, 74, 55fvmptf 5696 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  /\  ( [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )  e.  _V )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) ) )
7660, 75mpan2 652 . . . . . . . . . . . . . 14  |-  ( y  e.  A  ->  (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) ) `
 y )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 ) ) )
7776adantr 451 . . . . . . . . . . . . 13  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  C )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) ) )
78 ovex 5967 . . . . . . . . . . . . . . 15  |-  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  [_ y  /  x ]_ C )  e. 
_V
7962, 63, 65nfov 5965 . . . . . . . . . . . . . . . 16  |-  F/_ x
( [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  [_ y  /  x ]_ C
)
8069, 71oveq12d 5960 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( if ( 0  <_  B ,  B ,  0 )  +  C )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  + 
[_ y  /  x ]_ C ) )
81 eqid 2358 . . . . . . . . . . . . . . . 16  |-  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  =  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )
8261, 79, 80, 81fvmptf 5696 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  /\  ( [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  [_ y  /  x ]_ C
)  e.  _V )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  + 
[_ y  /  x ]_ C ) )
8378, 82mpan2 652 . . . . . . . . . . . . . 14  |-  ( y  e.  A  ->  (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `  y )  =  (
[_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  [_ y  /  x ]_ C
) )
8483adantr 451 . . . . . . . . . . . . 13  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  C )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  + 
[_ y  /  x ]_ C ) )
8559, 77, 843eqtr4d 2400 . . . . . . . . . . . 12  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  C )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) )
8685ex 423 . . . . . . . . . . 11  |-  ( y  e.  A  ->  ( [ y  /  x ] 0  <_  C  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) ) )
8786ss2rabi 3331 . . . . . . . . . 10  |-  { y  e.  A  |  [
y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) }
88 ovex 5967 . . . . . . . . . . . 12  |-  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) )  e.  _V
8988, 55fnmpti 5451 . . . . . . . . . . 11  |-  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  Fn  A
90 ovex 5967 . . . . . . . . . . . 12  |-  ( if ( 0  <_  B ,  B ,  0 )  +  C )  e. 
_V
9190, 81fnmpti 5451 . . . . . . . . . . 11  |-  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A
92 ssrab2 3334 . . . . . . . . . . . . 13  |-  { y  e.  A  |  [
y  /  x ]
0  <_  C }  C_  A
93 fnreseql 5715 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  Fn  A  /\  { y  e.  A  |  [ y  /  x ] 0  <_  C }  C_  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  C }
)  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  C }
)  <->  { y  e.  A  |  [ y  /  x ] 0  <_  C }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) ) ) )
9492, 93mp3an3 1266 . . . . . . . . . . . 12  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  Fn  A
)  ->  ( (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  <->  { y  e.  A  |  [
y  /  x ]
0  <_  C }  C_ 
dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) ) ) )
95 fndmin 5712 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  Fn  A
)  ->  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) )  =  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) } )
9695sseq2d 3282 . . . . . . . . . . . 12  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  Fn  A
)  ->  ( {
y  e.  A  |  [ y  /  x ] 0  <_  C }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) )  <->  { y  e.  A  |  [
y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) } ) )
9794, 96bitrd 244 . . . . . . . . . . 11  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  Fn  A
)  ->  ( (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  <->  { y  e.  A  |  [
y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) } ) )
9889, 91, 97mp2an 653 . . . . . . . . . 10  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  <->  { y  e.  A  |  [
y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y ) } )
9987, 98mpbir 200 . . . . . . . . 9  |-  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  C }
)  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  C }
)
10010, 4readdcld 8949 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  B ,  B ,  0 )  +  C )  e.  RR )
101100, 81fmptd 5764 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) : A --> RR )
102 iftrue 3647 . . . . . . . . . . . . . . . . . 18  |-  ( [ y  /  x ]
0  <_  B  ->  if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  =  [_ y  /  x ]_ B )
103102oveq1d 5957 . . . . . . . . . . . . . . . . 17  |-  ( [ y  /  x ]
0  <_  B  ->  ( if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  + 
[_ y  /  x ]_ C )  =  (
[_ y  /  x ]_ B  +  [_ y  /  x ]_ C ) )
104103adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  B )  ->  ( if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C )  =  ( [_ y  /  x ]_ B  +  [_ y  /  x ]_ C
) )
105 ovex 5967 . . . . . . . . . . . . . . . . . 18  |-  ( if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C )  e. 
_V
106 nfs1v 2111 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ x [ y  /  x ] 0  <_  B
107 nfcsb1v 3189 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ x [_ y  /  x ]_ B
108106, 107, 66nfif 3665 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ x if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )
109108, 63, 65nfov 5965 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C )
110 sbequ12 1924 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  (
0  <_  B  <->  [ y  /  x ] 0  <_  B ) )
111 csbeq1a 3165 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  B  =  [_ y  /  x ]_ B )
112110, 111, 72ifbieq12d 3663 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  if ( 0  <_  B ,  B ,  0 )  =  if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 ) )
113112, 71oveq12d 5960 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( if ( 0  <_  B ,  B ,  0 )  +  C )  =  ( if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C ) )
11461, 109, 113, 81fvmptf 5696 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  A  /\  ( if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  + 
[_ y  /  x ]_ C )  e.  _V )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C ) )
115105, 114mpan2 652 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  A  ->  (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `  y )  =  ( if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  + 
[_ y  /  x ]_ C ) )
116115adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  B )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C ) )
117 ovex 5967 . . . . . . . . . . . . . . . . . 18  |-  ( [_ y  /  x ]_ B  +  [_ y  /  x ]_ C )  e.  _V
118107, 63, 65nfov 5965 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( [_ y  /  x ]_ B  +  [_ y  /  x ]_ C )
119111, 71oveq12d 5960 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  ( B  +  C )  =  ( [_ y  /  x ]_ B  +  [_ y  /  x ]_ C ) )
120 eqid 2358 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  A  |->  ( B  +  C ) )  =  ( x  e.  A  |->  ( B  +  C ) )
12161, 118, 119, 120fvmptf 5696 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  A  /\  ( [_ y  /  x ]_ B  +  [_ y  /  x ]_ C )  e.  _V )  -> 
( ( x  e.  A  |->  ( B  +  C ) ) `  y )  =  (
[_ y  /  x ]_ B  +  [_ y  /  x ]_ C ) )
122117, 121mpan2 652 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  A  ->  (
( x  e.  A  |->  ( B  +  C
) ) `  y
)  =  ( [_ y  /  x ]_ B  +  [_ y  /  x ]_ C ) )
123122adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  B )  ->  ( ( x  e.  A  |->  ( B  +  C ) ) `  y )  =  (
[_ y  /  x ]_ B  +  [_ y  /  x ]_ C ) )
124104, 116, 1233eqtr4d 2400 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  B )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) )
125124ex 423 . . . . . . . . . . . . . 14  |-  ( y  e.  A  ->  ( [ y  /  x ] 0  <_  B  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) ) )
126125ss2rabi 3331 . . . . . . . . . . . . 13  |-  { y  e.  A  |  [
y  /  x ]
0  <_  B }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) }
127 ovex 5967 . . . . . . . . . . . . . . 15  |-  ( B  +  C )  e. 
_V
128127, 120fnmpti 5451 . . . . . . . . . . . . . 14  |-  ( x  e.  A  |->  ( B  +  C ) )  Fn  A
129 ssrab2 3334 . . . . . . . . . . . . . . . 16  |-  { y  e.  A  |  [
y  /  x ]
0  <_  B }  C_  A
130 fnreseql 5715 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( B  +  C ) )  Fn  A  /\  {
y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( B  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  i^i  (
x  e.  A  |->  ( B  +  C ) ) ) ) )
131129, 130mp3an3 1266 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( B  +  C ) )  Fn  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( B  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  i^i  (
x  e.  A  |->  ( B  +  C ) ) ) ) )
132 fndmin 5712 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( B  +  C ) )  Fn  A )  ->  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  i^i  ( x  e.  A  |->  ( B  +  C ) ) )  =  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) } )
133132sseq2d 3282 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( B  +  C ) )  Fn  A )  -> 
( { y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  i^i  ( x  e.  A  |->  ( B  +  C ) ) )  <->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) } ) )
134131, 133bitrd 244 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( B  +  C ) )  Fn  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( B  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) } ) )
13591, 128, 134mp2an 653 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( B  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  C_  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( B  +  C ) ) `  y ) } )
136126, 135mpbir 200 . . . . . . . . . . . 12  |-  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  B }
)  =  ( ( x  e.  A  |->  ( B  +  C ) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  B }
)
137 nfcv 2494 . . . . . . . . . . . . . . . . 17  |-  F/_ x A
138 nfcv 2494 . . . . . . . . . . . . . . . . 17  |-  F/_ y A
139 nfv 1619 . . . . . . . . . . . . . . . . 17  |-  F/ y 0  <_  B
140137, 138, 139, 106, 110cbvrab 2862 . . . . . . . . . . . . . . . 16  |-  { x  e.  A  |  0  <_  B }  =  {
y  e.  A  |  [ y  /  x ] 0  <_  B }
141 leloe 8995 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 0  e.  RR  /\  B  e.  RR )  ->  ( 0  <_  B  <->  ( 0  <  B  \/  0  =  B )
) )
1428, 1, 141sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <_  B  <->  ( 0  <  B  \/  0  =  B ) ) )
1431biantrurd 494 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <  B  <->  ( B  e.  RR  /\  0  < 
B ) ) )
144 repos 10829 . . . . . . . . . . . . . . . . . . . 20  |-  ( B  e.  ( 0 (,) 
+oo )  <->  ( B  e.  RR  /\  0  < 
B ) )
145143, 144syl6rbbr 255 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( B  e.  ( 0 (,)  +oo )  <->  0  <  B ) )
146 elsncg 3738 . . . . . . . . . . . . . . . . . . . . 21  |-  ( B  e.  RR  ->  ( B  e.  { 0 } 
<->  B  =  0 ) )
1471, 146syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  A )  ->  ( B  e.  { 0 } 
<->  B  =  0 ) )
148 eqcom 2360 . . . . . . . . . . . . . . . . . . . 20  |-  ( B  =  0  <->  0  =  B )
149147, 148syl6bb 252 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( B  e.  { 0 } 
<->  0  =  B ) )
150145, 149orbi12d 690 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  (
( B  e.  ( 0 (,)  +oo )  \/  B  e.  { 0 } )  <->  ( 0  <  B  \/  0  =  B ) ) )
151142, 150bitr4d 247 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <_  B  <->  ( B  e.  ( 0 (,)  +oo )  \/  B  e.  { 0 } ) ) )
152151rabbidva 2855 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { x  e.  A  |  0  <_  B }  =  { x  e.  A  |  ( B  e.  ( 0 (,)  +oo )  \/  B  e.  { 0 } ) } )
153140, 152syl5eqr 2404 . . . . . . . . . . . . . . 15  |-  ( ph  ->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  =  { x  e.  A  |  ( B  e.  ( 0 (,)  +oo )  \/  B  e.  { 0 } ) } )
154 eqid 2358 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  B )
155154mptpreima 5245 . . . . . . . . . . . . . . . . 17  |-  ( `' ( x  e.  A  |->  B ) " (
0 (,)  +oo ) )  =  { x  e.  A  |  B  e.  ( 0 (,)  +oo ) }
156154mptpreima 5245 . . . . . . . . . . . . . . . . 17  |-  ( `' ( x  e.  A  |->  B ) " {
0 } )  =  { x  e.  A  |  B  e.  { 0 } }
157155, 156uneq12i 3403 . . . . . . . . . . . . . . . 16  |-  ( ( `' ( x  e.  A  |->  B ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  B ) " { 0 } ) )  =  ( { x  e.  A  |  B  e.  ( 0 (,)  +oo ) }  u.  { x  e.  A  |  B  e.  { 0 } } )
158 unrab 3515 . . . . . . . . . . . . . . . 16  |-  ( { x  e.  A  |  B  e.  ( 0 (,)  +oo ) }  u.  { x  e.  A  |  B  e.  { 0 } } )  =  {
x  e.  A  | 
( B  e.  ( 0 (,)  +oo )  \/  B  e.  { 0 } ) }
159157, 158eqtri 2378 . . . . . . . . . . . . . . 15  |-  ( ( `' ( x  e.  A  |->  B ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  B ) " { 0 } ) )  =  { x  e.  A  |  ( B  e.  ( 0 (,)  +oo )  \/  B  e.  { 0 } ) }
160153, 159syl6eqr 2408 . . . . . . . . . . . . . 14  |-  ( ph  ->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  =  ( ( `' ( x  e.  A  |->  B ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  B ) " { 0 } ) ) )
161 iblmbf 19220 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  A  |->  B )  e.  L ^1 
->  ( x  e.  A  |->  B )  e. MblFn )
16242, 161syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  A  |->  B )  e. MblFn )
1631, 154fmptd 5764 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( x  e.  A  |->  B ) : A --> RR )
164 mbfima 19085 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  A  |->  B )  e. MblFn  /\  (
x  e.  A  |->  B ) : A --> RR )  ->  ( `' ( x  e.  A  |->  B ) " ( 0 (,)  +oo ) )  e. 
dom  vol )
165 mbfimasn 19087 . . . . . . . . . . . . . . . . 17  |-  ( ( ( x  e.  A  |->  B )  e. MblFn  /\  (
x  e.  A  |->  B ) : A --> RR  /\  0  e.  RR )  ->  ( `' ( x  e.  A  |->  B )
" { 0 } )  e.  dom  vol )
1668, 165mp3an3 1266 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  A  |->  B )  e. MblFn  /\  (
x  e.  A  |->  B ) : A --> RR )  ->  ( `' ( x  e.  A  |->  B ) " { 0 } )  e.  dom  vol )
167 unmbl 18993 . . . . . . . . . . . . . . . 16  |-  ( ( ( `' ( x  e.  A  |->  B )
" ( 0 (,) 
+oo ) )  e. 
dom  vol  /\  ( `' ( x  e.  A  |->  B ) " {
0 } )  e. 
dom  vol )  ->  (
( `' ( x  e.  A  |->  B )
" ( 0 (,) 
+oo ) )  u.  ( `' ( x  e.  A  |->  B )
" { 0 } ) )  e.  dom  vol )
168164, 166, 167syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  A  |->  B )  e. MblFn  /\  (
x  e.  A  |->  B ) : A --> RR )  ->  ( ( `' ( x  e.  A  |->  B ) " (
0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  B ) " { 0 } ) )  e. 
dom  vol )
169162, 163, 168syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( `' ( x  e.  A  |->  B ) " ( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  B )
" { 0 } ) )  e.  dom  vol )
170160, 169eqeltrd 2432 . . . . . . . . . . . . 13  |-  ( ph  ->  { y  e.  A  |  [ y  /  x ] 0  <_  B }  e.  dom  vol )
171 mbfres 19097 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( B  +  C
) )  e. MblFn  /\  {
y  e.  A  |  [ y  /  x ] 0  <_  B }  e.  dom  vol )  ->  ( ( x  e.  A  |->  ( B  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  e. MblFn )
17244, 170, 171syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( x  e.  A  |->  ( B  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  e. MblFn )
173136, 172syl5eqel 2442 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  B } )  e. MblFn )
174 iffalse 3648 . . . . . . . . . . . . . . . . . 18  |-  ( -. 
[ y  /  x ] 0  <_  B  ->  if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  =  0 )
175174oveq1d 5957 . . . . . . . . . . . . . . . . 17  |-  ( -. 
[ y  /  x ] 0  <_  B  ->  ( if ( [ y  /  x ]
0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C )  =  ( 0  +  [_ y  /  x ]_ C
) )
176175adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  B
)  ->  ( if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C )  =  ( 0  +  [_ y  /  x ]_ C
) )
177115adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  B
)  ->  ( (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( if ( [ y  /  x ] 0  <_  B ,  [_ y  /  x ]_ B ,  0 )  +  [_ y  /  x ]_ C ) )
178 ovex 5967 . . . . . . . . . . . . . . . . . 18  |-  ( 0  +  [_ y  /  x ]_ C )  e. 
_V
17966, 63, 65nfov 5965 . . . . . . . . . . . . . . . . . . 19  |-  F/_ x
( 0  +  [_ y  /  x ]_ C
)
18071oveq2d 5958 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
0  +  C )  =  ( 0  + 
[_ y  /  x ]_ C ) )
181 eqid 2358 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  A  |->  ( 0  +  C ) )  =  ( x  e.  A  |->  ( 0  +  C ) )
18261, 179, 180, 181fvmptf 5696 . . . . . . . . . . . . . . . . . 18  |-  ( ( y  e.  A  /\  ( 0  +  [_ y  /  x ]_ C
)  e.  _V )  ->  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y )  =  ( 0  +  [_ y  /  x ]_ C ) )
183178, 182mpan2 652 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  A  ->  (
( x  e.  A  |->  ( 0  +  C
) ) `  y
)  =  ( 0  +  [_ y  /  x ]_ C ) )
184183adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  B
)  ->  ( (
x  e.  A  |->  ( 0  +  C ) ) `  y )  =  ( 0  + 
[_ y  /  x ]_ C ) )
185176, 177, 1843eqtr4d 2400 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  B
)  ->  ( (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) )
186185ex 423 . . . . . . . . . . . . . 14  |-  ( y  e.  A  ->  ( -.  [ y  /  x ] 0  <_  B  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) ) )
187186ss2rabi 3331 . . . . . . . . . . . . 13  |-  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) ) `
 y )  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) }
188 ovex 5967 . . . . . . . . . . . . . . 15  |-  ( 0  +  C )  e. 
_V
189188, 181fnmpti 5451 . . . . . . . . . . . . . 14  |-  ( x  e.  A  |->  ( 0  +  C ) )  Fn  A
190 ssrab2 3334 . . . . . . . . . . . . . . . 16  |-  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }  C_  A
191 fnreseql 5715 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( 0  +  C ) )  Fn  A  /\  {
y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  C_  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( 0  +  C
) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  i^i  (
x  e.  A  |->  ( 0  +  C ) ) ) ) )
192190, 191mp3an3 1266 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( 0  +  C ) )  Fn  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( 0  +  C
) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  i^i  (
x  e.  A  |->  ( 0  +  C ) ) ) ) )
193 fndmin 5712 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( 0  +  C ) )  Fn  A )  ->  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  i^i  ( x  e.  A  |->  ( 0  +  C ) ) )  =  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) } )
194193sseq2d 3282 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( 0  +  C ) )  Fn  A )  -> 
( { y  e.  A  |  -.  [
y  /  x ]
0  <_  B }  C_ 
dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  i^i  ( x  e.  A  |->  ( 0  +  C ) ) )  <->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  C_  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) } ) )
195192, 194bitrd 244 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  Fn  A  /\  ( x  e.  A  |->  ( 0  +  C ) )  Fn  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( 0  +  C
) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  C_  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) } ) )
19691, 189, 195mp2an 653 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  =  ( ( x  e.  A  |->  ( 0  +  C
) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)  <->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  C_  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) ) `  y
)  =  ( ( x  e.  A  |->  ( 0  +  C ) ) `  y ) } )
197187, 196mpbir 200 . . . . . . . . . . . 12  |-  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  C
) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)  =  ( ( x  e.  A  |->  ( 0  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)
1984recnd 8948 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  C  e.  CC )
199198addid2d 9100 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  (
0  +  C )  =  C )
200199mpteq2dva 4185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  A  |->  ( 0  +  C
) )  =  ( x  e.  A  |->  C ) )
201 iblmbf 19220 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  |->  C )  e.  L ^1 
->  ( x  e.  A  |->  C )  e. MblFn )
20243, 201syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( x  e.  A  |->  C )  e. MblFn )
203200, 202eqeltrd 2432 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x  e.  A  |->  ( 0  +  C
) )  e. MblFn )
204154mptpreima 5245 . . . . . . . . . . . . . . 15  |-  ( `' ( x  e.  A  |->  B ) " (  -oo (,) 0 ) )  =  { x  e.  A  |  B  e.  (  -oo (,) 0
) }
2051biantrurd 494 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  x  e.  A )  ->  ( B  <  0  <->  ( B  e.  RR  /\  B  <  0 ) ) )
206 0xr 8965 . . . . . . . . . . . . . . . . . . . 20  |-  0  e.  RR*
207 elioomnf 10827 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  RR*  ->  ( B  e.  (  -oo (,) 0 )  <->  ( B  e.  RR  /\  B  <  0 ) ) )
208206, 207ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( B  e.  (  -oo (,) 0 )  <->  ( B  e.  RR  /\  B  <  0 ) )
209205, 208syl6bbr 254 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( B  <  0  <->  B  e.  (  -oo (,) 0 ) ) )
210 ltnle 8989 . . . . . . . . . . . . . . . . . . 19  |-  ( ( B  e.  RR  /\  0  e.  RR )  ->  ( B  <  0  <->  -.  0  <_  B )
)
2111, 8, 210sylancl 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  x  e.  A )  ->  ( B  <  0  <->  -.  0  <_  B ) )
212209, 211bitr3d 246 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( B  e.  (  -oo (,) 0 )  <->  -.  0  <_  B ) )
213212rabbidva 2855 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { x  e.  A  |  B  e.  (  -oo (,) 0 ) }  =  { x  e.  A  |  -.  0  <_  B } )
214 nfv 1619 . . . . . . . . . . . . . . . . 17  |-  F/ y  -.  0  <_  B
215106nfn 1794 . . . . . . . . . . . . . . . . 17  |-  F/ x  -.  [ y  /  x ] 0  <_  B
216110notbid 285 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  ( -.  0  <_  B  <->  -.  [ y  /  x ] 0  <_  B ) )
217137, 138, 214, 215, 216cbvrab 2862 . . . . . . . . . . . . . . . 16  |-  { x  e.  A  |  -.  0  <_  B }  =  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }
218213, 217syl6eq 2406 . . . . . . . . . . . . . . 15  |-  ( ph  ->  { x  e.  A  |  B  e.  (  -oo (,) 0 ) }  =  { y  e.  A  |  -.  [
y  /  x ]
0  <_  B }
)
219204, 218syl5eq 2402 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' ( x  e.  A  |->  B )
" (  -oo (,) 0 ) )  =  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )
220 mbfima 19085 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  A  |->  B )  e. MblFn  /\  (
x  e.  A  |->  B ) : A --> RR )  ->  ( `' ( x  e.  A  |->  B ) " (  -oo (,) 0 ) )  e. 
dom  vol )
221162, 163, 220syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( `' ( x  e.  A  |->  B )
" (  -oo (,) 0 ) )  e. 
dom  vol )
222219, 221eqeltrrd 2433 . . . . . . . . . . . . 13  |-  ( ph  ->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  e.  dom  vol )
223 mbfres 19097 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( 0  +  C
) )  e. MblFn  /\  {
y  e.  A  |  -.  [ y  /  x ] 0  <_  B }  e.  dom  vol )  ->  ( ( x  e.  A  |->  ( 0  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  e. MblFn )
224203, 222, 223syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( x  e.  A  |->  ( 0  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  e. MblFn )
225197, 224syl5eqel 2442 . . . . . . . . . . 11  |-  ( ph  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  e. MblFn )
226 rabxm 3553 . . . . . . . . . . . . 13  |-  A  =  ( { y  e.  A  |  [ y  /  x ] 0  <_  B }  u.  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )
227226eqcomi 2362 . . . . . . . . . . . 12  |-  ( { y  e.  A  |  [ y  /  x ] 0  <_  B }  u.  { y  e.  A  |  -.  [ y  /  x ]
0  <_  B }
)  =  A
228227a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  ( { y  e.  A  |  [ y  /  x ] 0  <_  B }  u.  { y  e.  A  |  -.  [ y  /  x ] 0  <_  B } )  =  A )
229101, 173, 225, 228mbfres2 19098 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  e. MblFn
)
230 nfv 1619 . . . . . . . . . . . . 13  |-  F/ y 0  <_  C
231137, 138, 230, 64, 70cbvrab 2862 . . . . . . . . . . . 12  |-  { x  e.  A  |  0  <_  C }  =  {
y  e.  A  |  [ y  /  x ] 0  <_  C }
232 leloe 8995 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  C  e.  RR )  ->  ( 0  <_  C  <->  ( 0  <  C  \/  0  =  C )
) )
2338, 4, 232sylancr 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <_  C  <->  ( 0  <  C  \/  0  =  C ) ) )
2344biantrurd 494 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <  C  <->  ( C  e.  RR  /\  0  < 
C ) ) )
235 repos 10829 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  ( 0 (,) 
+oo )  <->  ( C  e.  RR  /\  0  < 
C ) )
236234, 235syl6rbbr 255 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( C  e.  ( 0 (,)  +oo )  <->  0  <  C ) )
237 elsncg 3738 . . . . . . . . . . . . . . . . . 18  |-  ( C  e.  RR  ->  ( C  e.  { 0 } 
<->  C  =  0 ) )
2384, 237syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  x  e.  A )  ->  ( C  e.  { 0 } 
<->  C  =  0 ) )
239 eqcom 2360 . . . . . . . . . . . . . . . . 17  |-  ( C  =  0  <->  0  =  C )
240238, 239syl6bb 252 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( C  e.  { 0 } 
<->  0  =  C ) )
241236, 240orbi12d 690 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  (
( C  e.  ( 0 (,)  +oo )  \/  C  e.  { 0 } )  <->  ( 0  <  C  \/  0  =  C ) ) )
242233, 241bitr4d 247 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  (
0  <_  C  <->  ( C  e.  ( 0 (,)  +oo )  \/  C  e.  { 0 } ) ) )
243242rabbidva 2855 . . . . . . . . . . . . 13  |-  ( ph  ->  { x  e.  A  |  0  <_  C }  =  { x  e.  A  |  ( C  e.  ( 0 (,)  +oo )  \/  C  e.  { 0 } ) } )
244 eqid 2358 . . . . . . . . . . . . . . . 16  |-  ( x  e.  A  |->  C )  =  ( x  e.  A  |->  C )
245244mptpreima 5245 . . . . . . . . . . . . . . 15  |-  ( `' ( x  e.  A  |->  C ) " (
0 (,)  +oo ) )  =  { x  e.  A  |  C  e.  ( 0 (,)  +oo ) }
246244mptpreima 5245 . . . . . . . . . . . . . . 15  |-  ( `' ( x  e.  A  |->  C ) " {
0 } )  =  { x  e.  A  |  C  e.  { 0 } }
247245, 246uneq12i 3403 . . . . . . . . . . . . . 14  |-  ( ( `' ( x  e.  A  |->  C ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  C ) " { 0 } ) )  =  ( { x  e.  A  |  C  e.  ( 0 (,)  +oo ) }  u.  { x  e.  A  |  C  e.  { 0 } } )
248 unrab 3515 . . . . . . . . . . . . . 14  |-  ( { x  e.  A  |  C  e.  ( 0 (,)  +oo ) }  u.  { x  e.  A  |  C  e.  { 0 } } )  =  {
x  e.  A  | 
( C  e.  ( 0 (,)  +oo )  \/  C  e.  { 0 } ) }
249247, 248eqtri 2378 . . . . . . . . . . . . 13  |-  ( ( `' ( x  e.  A  |->  C ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  C ) " { 0 } ) )  =  { x  e.  A  |  ( C  e.  ( 0 (,)  +oo )  \/  C  e.  { 0 } ) }
250243, 249syl6eqr 2408 . . . . . . . . . . . 12  |-  ( ph  ->  { x  e.  A  |  0  <_  C }  =  ( ( `' ( x  e.  A  |->  C ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  C ) " { 0 } ) ) )
251231, 250syl5eqr 2404 . . . . . . . . . . 11  |-  ( ph  ->  { y  e.  A  |  [ y  /  x ] 0  <_  C }  =  ( ( `' ( x  e.  A  |->  C ) "
( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  C ) " { 0 } ) ) )
2524, 244fmptd 5764 . . . . . . . . . . . 12  |-  ( ph  ->  ( x  e.  A  |->  C ) : A --> RR )
253 mbfima 19085 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  C )  e. MblFn  /\  (
x  e.  A  |->  C ) : A --> RR )  ->  ( `' ( x  e.  A  |->  C ) " ( 0 (,)  +oo ) )  e. 
dom  vol )
254 mbfimasn 19087 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  A  |->  C )  e. MblFn  /\  (
x  e.  A  |->  C ) : A --> RR  /\  0  e.  RR )  ->  ( `' ( x  e.  A  |->  C )
" { 0 } )  e.  dom  vol )
2558, 254mp3an3 1266 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  C )  e. MblFn  /\  (
x  e.  A  |->  C ) : A --> RR )  ->  ( `' ( x  e.  A  |->  C ) " { 0 } )  e.  dom  vol )
256 unmbl 18993 . . . . . . . . . . . . 13  |-  ( ( ( `' ( x  e.  A  |->  C )
" ( 0 (,) 
+oo ) )  e. 
dom  vol  /\  ( `' ( x  e.  A  |->  C ) " {
0 } )  e. 
dom  vol )  ->  (
( `' ( x  e.  A  |->  C )
" ( 0 (,) 
+oo ) )  u.  ( `' ( x  e.  A  |->  C )
" { 0 } ) )  e.  dom  vol )
257253, 255, 256syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( x  e.  A  |->  C )  e. MblFn  /\  (
x  e.  A  |->  C ) : A --> RR )  ->  ( ( `' ( x  e.  A  |->  C ) " (
0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  C ) " { 0 } ) )  e. 
dom  vol )
258202, 252, 257syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( ( `' ( x  e.  A  |->  C ) " ( 0 (,)  +oo ) )  u.  ( `' ( x  e.  A  |->  C )
" { 0 } ) )  e.  dom  vol )
259251, 258eqeltrd 2432 . . . . . . . . . 10  |-  ( ph  ->  { y  e.  A  |  [ y  /  x ] 0  <_  C }  e.  dom  vol )
260 mbfres 19097 . . . . . . . . . 10  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  e. MblFn  /\  { y  e.  A  |  [ y  /  x ] 0  <_  C }  e.  dom  vol )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  e. MblFn )
261229, 259, 260syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  C ) )  |`  { y  e.  A  |  [ y  /  x ] 0  <_  C } )  e. MblFn )
26299, 261syl5eqel 2442 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  |`  { y  e.  A  |  [
y  /  x ]
0  <_  C }
)  e. MblFn )
263 iffalse 3648 . . . . . . . . . . . . . . 15  |-  ( -. 
[ y  /  x ] 0  <_  C  ->  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 )  =  0 )
264263oveq2d 5958 . . . . . . . . . . . . . 14  |-  ( -. 
[ y  /  x ] 0  <_  C  ->  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ] 0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  0 ) )
265264adantl 452 . . . . . . . . . . . . 13  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  C
)  ->  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  0 ) )
26676adantr 451 . . . . . . . . . . . . 13  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  C
)  ->  ( (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y
)  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  if ( [ y  /  x ]
0  <_  C ,  [_ y  /  x ]_ C ,  0 ) ) )
267 ovex 5967 . . . . . . . . . . . . . . 15  |-  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  0 )  e. 
_V
26862, 63, 66nfov 5965 . . . . . . . . . . . . . . . 16  |-  F/_ x
( [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  0 )
26969oveq1d 5957 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( if ( 0  <_  B ,  B ,  0 )  +  0 )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  0 ) )
270 eqid 2358 . . . . . . . . . . . . . . . 16  |-  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  =  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )
27161, 268, 269, 270fvmptf 5696 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  A  /\  ( [_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  0 )  e.  _V )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y )  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  0 ) )
272267, 271mpan2 652 . . . . . . . . . . . . . 14  |-  ( y  e.  A  ->  (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `  y )  =  (
[_ y  /  x ]_ if ( 0  <_  B ,  B , 
0 )  +  0 ) )
273272adantr 451 . . . . . . . . . . . . 13  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  C
)  ->  ( (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) ) `  y
)  =  ( [_ y  /  x ]_ if ( 0  <_  B ,  B ,  0 )  +  0 ) )
274265, 266, 2733eqtr4d 2400 . . . . . . . . . . . 12  |-  ( ( y  e.  A  /\  -.  [ y  /  x ] 0  <_  C
)  ->  ( (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y
)  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) ) `  y
) )
275274ex 423 . . . . . . . . . . 11  |-  ( y  e.  A  ->  ( -.  [ y  /  x ] 0  <_  C  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y ) ) )
276275ss2rabi 3331 . . . . . . . . . 10  |-  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y ) }
277 ovex 5967 . . . . . . . . . . . 12  |-  ( if ( 0  <_  B ,  B ,  0 )  +  0 )  e. 
_V
278277, 270fnmpti 5451 . . . . . . . . . . 11  |-  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  Fn  A
279 ssrab2 3334 . . . . . . . . . . . . 13  |-  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }  C_  A
280 fnreseql 5715 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  Fn  A  /\  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C }  C_  A )  -> 
( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }
)  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }
)  <->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) ) ) ) )
281279, 280mp3an3 1266 . . . . . . . . . . . 12  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  Fn  A
)  ->  ( (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  <->  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }  C_ 
dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) ) ) )
282 fndmin 5712 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  Fn  A
)  ->  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) ) )  =  { y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y ) } )
283282sseq2d 3282 . . . . . . . . . . . 12  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  Fn  A
)  ->  ( {
y  e.  A  |  -.  [ y  /  x ] 0  <_  C }  C_  dom  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  i^i  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) ) )  <->  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y ) } ) )
284281, 283bitrd 244 . . . . . . . . . . 11  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  Fn  A  /\  (
x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  Fn  A
)  ->  ( (
( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  <->  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y ) } ) )
28589, 278, 284mp2an 653 . . . . . . . . . 10  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  <->  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }  C_ 
{ y  e.  A  |  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) `  y )  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) ) `
 y ) } )
286276, 285mpbir 200 . . . . . . . . 9  |-  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }
)  =  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B , 
0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }
)
28711addid1d 9099 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  B ,  B ,  0 )  +  0 )  =  if ( 0  <_  B ,  B , 
0 ) )
288287mpteq2dva 4185 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  =  ( x  e.  A  |->  if ( 0  <_  B ,  B , 
0 ) ) )
289 iblmbf 19220 . . . . . . . . . . . 12  |-  ( ( x  e.  A  |->  if ( 0  <_  B ,  B ,  0 ) )  e.  L ^1 
->  ( x  e.  A  |->  if ( 0  <_  B ,  B , 
0 ) )  e. MblFn
)
29051, 289syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  A  |->  if ( 0  <_  B ,  B , 
0 ) )  e. MblFn
)
291288, 290eqeltrd 2432 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  e. MblFn
)
292244mptpreima 5245 . . . . . . . . . . . . 13  |-  ( `' ( x  e.  A  |->  C ) " (  -oo (,) 0 ) )  =  { x  e.  A  |  C  e.  (  -oo (,) 0
) }
2934biantrurd 494 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  A )  ->  ( C  <  0  <->  ( C  e.  RR  /\  C  <  0 ) ) )
294 elioomnf 10827 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  RR*  ->  ( C  e.  (  -oo (,) 0 )  <->  ( C  e.  RR  /\  C  <  0 ) ) )
295206, 294ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( C  e.  (  -oo (,) 0 )  <->  ( C  e.  RR  /\  C  <  0 ) )
296293, 295syl6bbr 254 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  ( C  <  0  <->  C  e.  (  -oo (,) 0 ) ) )
297 ltnle 8989 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  RR  /\  0  e.  RR )  ->  ( C  <  0  <->  -.  0  <_  C )
)
2984, 8, 297sylancl 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  A )  ->  ( C  <  0  <->  -.  0  <_  C ) )
299296, 298bitr3d 246 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  ( C  e.  (  -oo (,) 0 )  <->  -.  0  <_  C ) )
300299rabbidva 2855 . . . . . . . . . . . . 13  |-  ( ph  ->  { x  e.  A  |  C  e.  (  -oo (,) 0 ) }  =  { x  e.  A  |  -.  0  <_  C } )
301292, 300syl5eq 2402 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' ( x  e.  A  |->  C )
" (  -oo (,) 0 ) )  =  { x  e.  A  |  -.  0  <_  C } )
302 nfv 1619 . . . . . . . . . . . . 13  |-  F/ y  -.  0  <_  C
30364nfn 1794 . . . . . . . . . . . . 13  |-  F/ x  -.  [ y  /  x ] 0  <_  C
30470notbid 285 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( -.  0  <_  C  <->  -.  [ y  /  x ] 0  <_  C ) )
305137, 138, 302, 303, 304cbvrab 2862 . . . . . . . . . . . 12  |-  { x  e.  A  |  -.  0  <_  C }  =  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C }
306301, 305syl6eq 2406 . . . . . . . . . . 11  |-  ( ph  ->  ( `' ( x  e.  A  |->  C )
" (  -oo (,) 0 ) )  =  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )
307 mbfima 19085 . . . . . . . . . . . 12  |-  ( ( ( x  e.  A  |->  C )  e. MblFn  /\  (
x  e.  A  |->  C ) : A --> RR )  ->  ( `' ( x  e.  A  |->  C ) " (  -oo (,) 0 ) )  e. 
dom  vol )
308202, 252, 307syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( `' ( x  e.  A  |->  C )
" (  -oo (,) 0 ) )  e. 
dom  vol )
309306, 308eqeltrrd 2433 . . . . . . . . . 10  |-  ( ph  ->  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C }  e.  dom  vol )
310 mbfres 19097 . . . . . . . . . 10  |-  ( ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  e. MblFn  /\  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C }  e.  dom  vol )  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  e. MblFn )
311291, 309, 310syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  0 ) )  |`  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  e. MblFn )
312286, 311syl5eqel 2442 . . . . . . . 8  |-  ( ph  ->  ( ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  |`  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }
)  e. MblFn )
313 rabxm 3553 . . . . . . . . . 10  |-  A  =  ( { y  e.  A  |  [ y  /  x ] 0  <_  C }  u.  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )
314313eqcomi 2362 . . . . . . . . 9  |-  ( { y  e.  A  |  [ y  /  x ] 0  <_  C }  u.  { y  e.  A  |  -.  [ y  /  x ]
0  <_  C }
)  =  A
315314a1i 10 . . . . . . . 8  |-  ( ph  ->  ( { y  e.  A  |  [ y  /  x ] 0  <_  C }  u.  { y  e.  A  |  -.  [ y  /  x ] 0  <_  C } )  =  A )
31656, 262, 312, 315mbfres2 19098 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  e. MblFn )
31710, 51, 13, 54, 316ibladdnc 25497 . . . . . 6  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) )  e.  L ^1 )
31830, 32readdcld 8949 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  ( if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C ) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  e.  RR )
319 eqid 2358 . . . . . . . 8  |-  ( x  e.  A  |->  ( if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C ) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) )  =  ( x  e.  A  |->  ( if ( 0  <_  -u ( B  +  C
) ,  -u ( B  +  C ) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) ) )
320318, 319fmptd 5764 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  |->  ( if ( 0  <_  -u ( B  +  C ) ,  -u ( B  +  C
) ,  0 )  +  ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) ) ) : A --> RR )
321 iftrue 3647 . . . . . . . . . . . . . 14  |-  ( [ y  /  x ]
0  <_  -u ( B  +  C )  ->  if ( [ y  /  x ] 0  <_  -u ( B  +  C ) ,  [_ y  /  x ]_ -u ( B  +  C ) ,  0 )  =  [_ y  /  x ]_ -u ( B  +  C )
)
322321oveq1d 5957 . . . . . . . . . . . . 13  |-  ( [ y  /  x ]
0  <_  -u ( B  +  C )  -> 
( if ( [ y  /  x ]
0  <_  -u ( B  +  C ) , 
[_ y  /  x ]_ -u ( B  +  C ) ,  0 )  +  [_ y  /  x ]_ ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C ,  0 ) ) )  =  ( [_ y  /  x ]_ -u ( B  +  C )  +  [_ y  /  x ]_ ( if ( 0  <_  B ,  B ,  0 )  +  if ( 0  <_  C ,  C , 
0 ) ) ) )
323322adantl 452 . . . . . . . . . . . 12  |-  ( ( y  e.  A  /\  [ y  /  x ]
0  <_  -u ( B  +  C