MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvlipcn Structured version   Unicode version

Theorem dvlipcn 22521
Description: A complex function with derivative bounded by  M on an open ball is Lipschitz continuous with Lipschitz constant equal to  M. (Contributed by Mario Carneiro, 18-Mar-2015.)
Hypotheses
Ref Expression
dvlipcn.x  |-  ( ph  ->  X  C_  CC )
dvlipcn.f  |-  ( ph  ->  F : X --> CC )
dvlipcn.a  |-  ( ph  ->  A  e.  CC )
dvlipcn.r  |-  ( ph  ->  R  e.  RR* )
dvlipcn.b  |-  B  =  ( A ( ball `  ( abs  o.  -  ) ) R )
dvlipcn.d  |-  ( ph  ->  B  C_  dom  ( CC 
_D  F ) )
dvlipcn.m  |-  ( ph  ->  M  e.  RR )
dvlipcn.l  |-  ( (
ph  /\  x  e.  B )  ->  ( abs `  ( ( CC 
_D  F ) `  x ) )  <_  M )
Assertion
Ref Expression
dvlipcn  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( abs `  (
( F `  Y
)  -  ( F `
 Z ) ) )  <_  ( M  x.  ( abs `  ( Y  -  Z )
) ) )
Distinct variable groups:    x, B    x, F    x, M    ph, x
Allowed substitution hints:    A( x)    R( x)    X( x)    Y( x)    Z( x)

Proof of Theorem dvlipcn
Dummy variables  t 
y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1elunit 11664 . . 3  |-  1  e.  ( 0 [,] 1
)
2 0elunit 11663 . . 3  |-  0  e.  ( 0 [,] 1
)
3 0red 9614 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
0  e.  RR )
4 1red 9628 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
1  e.  RR )
5 dvlipcn.d . . . . . . . . . . . . . 14  |-  ( ph  ->  B  C_  dom  ( CC 
_D  F ) )
6 ssid 3518 . . . . . . . . . . . . . . . 16  |-  CC  C_  CC
76a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  C_  CC )
8 dvlipcn.f . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : X --> CC )
9 dvlipcn.x . . . . . . . . . . . . . . 15  |-  ( ph  ->  X  C_  CC )
107, 8, 9dvbss 22431 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( CC  _D  F )  C_  X
)
115, 10sstrd 3509 . . . . . . . . . . . . 13  |-  ( ph  ->  B  C_  X )
1211, 9sstrd 3509 . . . . . . . . . . . 12  |-  ( ph  ->  B  C_  CC )
1312adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  B  C_  CC )
14 simprl 756 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  Y  e.  B )
1513, 14sseldd 3500 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  Y  e.  CC )
1615adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  Y  e.  CC )
17 unitssre 11692 . . . . . . . . . . 11  |-  ( 0 [,] 1 )  C_  RR
18 ax-resscn 9566 . . . . . . . . . . 11  |-  RR  C_  CC
1917, 18sstri 3508 . . . . . . . . . 10  |-  ( 0 [,] 1 )  C_  CC
20 simpr 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  ( 0 [,] 1
) )
2119, 20sseldi 3497 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  t  e.  CC )
2216, 21mulcomd 9634 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  ( Y  x.  t )  =  ( t  x.  Y ) )
23 simprr 757 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  Z  e.  B )
2413, 23sseldd 3500 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  Z  e.  CC )
2524adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  Z  e.  CC )
26 iirev 21555 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,] 1 )  ->  (
1  -  t )  e.  ( 0 [,] 1 ) )
2726adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  -  t )  e.  ( 0 [,] 1 ) )
2819, 27sseldi 3497 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  (
1  -  t )  e.  CC )
2925, 28mulcomd 9634 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  ( Z  x.  ( 1  -  t ) )  =  ( ( 1  -  t )  x.  Z ) )
3022, 29oveq12d 6314 . . . . . . 7  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  =  ( ( t  x.  Y )  +  ( ( 1  -  t )  x.  Z
) ) )
31 dvlipcn.a . . . . . . . . 9  |-  ( ph  ->  A  e.  CC )
3231ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  A  e.  CC )
33 dvlipcn.r . . . . . . . . 9  |-  ( ph  ->  R  e.  RR* )
3433ad2antrr 725 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  R  e.  RR* )
3514adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  Y  e.  B )
3623adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  Z  e.  B )
37 dvlipcn.b . . . . . . . . 9  |-  B  =  ( A ( ball `  ( abs  o.  -  ) ) R )
3837blcvx 21429 . . . . . . . 8  |-  ( ( ( A  e.  CC  /\  R  e.  RR* )  /\  ( Y  e.  B  /\  Z  e.  B  /\  t  e.  (
0 [,] 1 ) ) )  ->  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  Z ) )  e.  B )
3932, 34, 35, 36, 20, 38syl23anc 1235 . . . . . . 7  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  (
( t  x.  Y
)  +  ( ( 1  -  t )  x.  Z ) )  e.  B )
4030, 39eqeltrd 2545 . . . . . 6  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  e.  B )
41 eqidd 2458 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  =  ( t  e.  ( 0 [,] 1 )  |->  ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )
428, 11fssresd 5758 . . . . . . . . 9  |-  ( ph  ->  ( F  |`  B ) : B --> CC )
4342feqmptd 5926 . . . . . . . 8  |-  ( ph  ->  ( F  |`  B )  =  ( z  e.  B  |->  ( ( F  |`  B ) `  z
) ) )
44 fvres 5886 . . . . . . . . 9  |-  ( z  e.  B  ->  (
( F  |`  B ) `
 z )  =  ( F `  z
) )
4544mpteq2ia 4539 . . . . . . . 8  |-  ( z  e.  B  |->  ( ( F  |`  B ) `  z ) )  =  ( z  e.  B  |->  ( F `  z
) )
4643, 45syl6eq 2514 . . . . . . 7  |-  ( ph  ->  ( F  |`  B )  =  ( z  e.  B  |->  ( F `  z ) ) )
4746adantr 465 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( F  |`  B )  =  ( z  e.  B  |->  ( F `  z ) ) )
48 fveq2 5872 . . . . . 6  |-  ( z  =  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) )  ->  ( F `  z )  =  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )
4940, 41, 47, 48fmptco 6065 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( F  |`  B )  o.  (
t  e.  ( 0 [,] 1 )  |->  ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  =  ( t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )
50 eqid 2457 . . . . . . . 8  |-  ( t  e.  ( 0 [,] 1 )  |->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  =  ( t  e.  ( 0 [,] 1
)  |->  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )
5140, 50fmptd 6056 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) : ( 0 [,] 1 ) --> B )
52 eqid 2457 . . . . . . . . 9  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
5352addcn 21495 . . . . . . . . . 10  |-  +  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
5453a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  +  e.  ( (
( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
55 cncfmptc 21541 . . . . . . . . . . . 12  |-  ( ( Y  e.  CC  /\  ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  Y )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
5619, 6, 55mp3an23 1316 . . . . . . . . . . 11  |-  ( Y  e.  CC  ->  (
t  e.  ( 0 [,] 1 )  |->  Y )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
5715, 56syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  Y )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
58 cncfmptid 21542 . . . . . . . . . . . 12  |-  ( ( ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  t )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
5919, 6, 58mp2an 672 . . . . . . . . . . 11  |-  ( t  e.  ( 0 [,] 1 )  |->  t )  e.  ( ( 0 [,] 1 ) -cn-> CC )
6059a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  t )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
6157, 60mulcncf 21985 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( Y  x.  t
) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
62 cncfmptc 21541 . . . . . . . . . . . 12  |-  ( ( Z  e.  CC  /\  ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  Z )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
6319, 6, 62mp3an23 1316 . . . . . . . . . . 11  |-  ( Z  e.  CC  ->  (
t  e.  ( 0 [,] 1 )  |->  Z )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
6424, 63syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  Z )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
6552subcn 21496 . . . . . . . . . . . 12  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
6665a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  -  e.  ( (
( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
67 ax-1cn 9567 . . . . . . . . . . . . 13  |-  1  e.  CC
68 cncfmptc 21541 . . . . . . . . . . . . 13  |-  ( ( 1  e.  CC  /\  ( 0 [,] 1
)  C_  CC  /\  CC  C_  CC )  ->  (
t  e.  ( 0 [,] 1 )  |->  1 )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )
6967, 19, 6, 68mp3an 1324 . . . . . . . . . . . 12  |-  ( t  e.  ( 0 [,] 1 )  |->  1 )  e.  ( ( 0 [,] 1 ) -cn-> CC )
7069a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  1 )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
7152, 66, 70, 60cncfmpt2f 21544 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( 1  -  t
) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
7264, 71mulcncf 21985 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( Z  x.  (
1  -  t ) ) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
7352, 54, 61, 72cncfmpt2f 21544 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
74 cncffvrn 21528 . . . . . . . 8  |-  ( ( B  C_  CC  /\  (
t  e.  ( 0 [,] 1 )  |->  ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) )  e.  ( ( 0 [,] 1 )
-cn-> CC ) )  -> 
( ( t  e.  ( 0 [,] 1
)  |->  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )  e.  ( ( 0 [,] 1 ) -cn-> B )  <-> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) : ( 0 [,] 1 ) --> B ) )
7513, 73, 74syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( t  e.  ( 0 [,] 1
)  |->  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )  e.  ( ( 0 [,] 1 ) -cn-> B )  <-> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) : ( 0 [,] 1 ) --> B ) )
7651, 75mpbird 232 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  e.  ( ( 0 [,] 1
) -cn-> B ) )
776a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  CC  C_  CC )
7842adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( F  |`  B ) : B --> CC )
7952cnfldtop 21417 . . . . . . . . . . . . . . 15  |-  ( TopOpen ` fld )  e.  Top
8052cnfldtopon 21416 . . . . . . . . . . . . . . . . 17  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
8180toponunii 19560 . . . . . . . . . . . . . . . 16  |-  CC  =  U. ( TopOpen ` fld )
8281restid 14851 . . . . . . . . . . . . . . 15  |-  ( (
TopOpen ` fld )  e.  Top  ->  ( ( TopOpen ` fld )t  CC )  =  (
TopOpen ` fld ) )
8379, 82ax-mp 5 . . . . . . . . . . . . . 14  |-  ( (
TopOpen ` fld )t  CC )  =  (
TopOpen ` fld )
8483eqcomi 2470 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( ( TopOpen ` fld )t  CC )
8552, 84dvres 22441 . . . . . . . . . . . 12  |-  ( ( ( CC  C_  CC  /\  F : X --> CC )  /\  ( X  C_  CC  /\  B  C_  CC ) )  ->  ( CC  _D  ( F  |`  B ) )  =  ( ( CC  _D  F )  |`  (
( int `  ( TopOpen
` fld
) ) `  B
) ) )
867, 8, 9, 12, 85syl22anc 1229 . . . . . . . . . . 11  |-  ( ph  ->  ( CC  _D  ( F  |`  B ) )  =  ( ( CC 
_D  F )  |`  ( ( int `  ( TopOpen
` fld
) ) `  B
) ) )
87 cnxmet 21406 . . . . . . . . . . . . . . . 16  |-  ( abs 
o.  -  )  e.  ( *Met `  CC )
8887a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( abs  o.  -  )  e.  ( *Met `  CC ) )
8952cnfldtopn 21415 . . . . . . . . . . . . . . . 16  |-  ( TopOpen ` fld )  =  ( MetOpen `  ( abs  o.  -  ) )
9089blopn 21129 . . . . . . . . . . . . . . 15  |-  ( ( ( abs  o.  -  )  e.  ( *Met `  CC )  /\  A  e.  CC  /\  R  e.  RR* )  ->  ( A ( ball `  ( abs  o.  -  ) ) R )  e.  (
TopOpen ` fld ) )
9188, 31, 33, 90syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A ( ball `  ( abs  o.  -  ) ) R )  e.  ( TopOpen ` fld ) )
9237, 91syl5eqel 2549 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  ( TopOpen ` fld )
)
93 isopn3i 19710 . . . . . . . . . . . . 13  |-  ( ( ( TopOpen ` fld )  e.  Top  /\  B  e.  ( TopOpen ` fld )
)  ->  ( ( int `  ( TopOpen ` fld ) ) `  B
)  =  B )
9479, 92, 93sylancr 663 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( int `  ( TopOpen
` fld
) ) `  B
)  =  B )
9594reseq2d 5283 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  _D  F )  |`  (
( int `  ( TopOpen
` fld
) ) `  B
) )  =  ( ( CC  _D  F
)  |`  B ) )
9686, 95eqtrd 2498 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  ( F  |`  B ) )  =  ( ( CC 
_D  F )  |`  B ) )
9796dmeqd 5215 . . . . . . . . 9  |-  ( ph  ->  dom  ( CC  _D  ( F  |`  B ) )  =  dom  (
( CC  _D  F
)  |`  B ) )
98 dmres 5304 . . . . . . . . . 10  |-  dom  (
( CC  _D  F
)  |`  B )  =  ( B  i^i  dom  ( CC  _D  F
) )
99 df-ss 3485 . . . . . . . . . . 11  |-  ( B 
C_  dom  ( CC  _D  F )  <->  ( B  i^i  dom  ( CC  _D  F ) )  =  B )
1005, 99sylib 196 . . . . . . . . . 10  |-  ( ph  ->  ( B  i^i  dom  ( CC  _D  F
) )  =  B )
10198, 100syl5eq 2510 . . . . . . . . 9  |-  ( ph  ->  dom  ( ( CC 
_D  F )  |`  B )  =  B )
10297, 101eqtrd 2498 . . . . . . . 8  |-  ( ph  ->  dom  ( CC  _D  ( F  |`  B ) )  =  B )
103102adantr 465 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  dom  ( CC  _D  ( F  |`  B ) )  =  B )
104 dvcn 22450 . . . . . . 7  |-  ( ( ( CC  C_  CC  /\  ( F  |`  B ) : B --> CC  /\  B  C_  CC )  /\  dom  ( CC  _D  ( F  |`  B ) )  =  B )  -> 
( F  |`  B )  e.  ( B -cn-> CC ) )
10577, 78, 13, 103, 104syl31anc 1231 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( F  |`  B )  e.  ( B -cn-> CC ) )
10676, 105cncfco 21537 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( F  |`  B )  o.  (
t  e.  ( 0 [,] 1 )  |->  ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
10749, 106eqeltrrd 2546 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  e.  ( ( 0 [,] 1
) -cn-> CC ) )
10818a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  RR  C_  CC )
10917a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( 0 [,] 1
)  C_  RR )
1108ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  F : X --> CC )
11111ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  B  C_  X )
112111, 40sseldd 3500 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  e.  X )
113110, 112ffvelrnd 6033 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 [,] 1
) )  ->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  e.  CC )
11452tgioo2 21434 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
115 1re 9612 . . . . . . . . 9  |-  1  e.  RR
116 iccntr 21452 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] 1 ) )  =  ( 0 (,) 1
) )
1173, 115, 116sylancl 662 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( int `  ( topGen `
 ran  (,) )
) `  ( 0 [,] 1 ) )  =  ( 0 (,) 1
) )
118108, 109, 113, 114, 52, 117dvmptntr 22500 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )  =  ( RR  _D  ( t  e.  ( 0 (,) 1 )  |->  ( F `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) ) ) ) )
119 reelprrecn 9601 . . . . . . . . 9  |-  RR  e.  { RR ,  CC }
120119a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  RR  e.  { RR ,  CC } )
121 cnelprrecn 9602 . . . . . . . . 9  |-  CC  e.  { RR ,  CC }
122121a1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  CC  e.  { RR ,  CC } )
123 ioossicc 11635 . . . . . . . . . 10  |-  ( 0 (,) 1 )  C_  ( 0 [,] 1
)
124123sseli 3495 . . . . . . . . 9  |-  ( t  e.  ( 0 (,) 1 )  ->  t  e.  ( 0 [,] 1
) )
125124, 40sylan2 474 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  e.  B )
12615, 24subcld 9950 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Y  -  Z
)  e.  CC )
127126adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( Y  -  Z )  e.  CC )
12811adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  B  C_  X )
129128sselda 3499 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  z  e.  B )  ->  z  e.  X )
1308adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  F : X --> CC )
131130ffvelrnda 6032 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  z  e.  X )  ->  ( F `  z )  e.  CC )
132129, 131syldan 470 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  z  e.  B )  ->  ( F `  z )  e.  CC )
133 fvex 5882 . . . . . . . . 9  |-  ( ( CC  _D  F ) `
 z )  e. 
_V
134133a1i 11 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  z  e.  B )  ->  (
( CC  _D  F
) `  z )  e.  _V )
13515adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  Y  e.  CC )
136124, 21sylan2 474 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  t  e.  CC )
137135, 136mulcld 9633 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( Y  x.  t )  e.  CC )
138 1red 9628 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  1  e.  RR )
139 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  RR )  ->  t  e.  RR )
140139recnd 9639 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  RR )  ->  t  e.  CC )
141 1red 9628 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  RR )  ->  1  e.  RR )
142120dvmptid 22486 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  RR  |->  t ) )  =  ( t  e.  RR  |->  1 ) )
143 ioossre 11611 . . . . . . . . . . . . . 14  |-  ( 0 (,) 1 )  C_  RR
144143a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( 0 (,) 1
)  C_  RR )
145 iooretop 21399 . . . . . . . . . . . . . 14  |-  ( 0 (,) 1 )  e.  ( topGen `  ran  (,) )
146145a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( 0 (,) 1
)  e.  ( topGen ` 
ran  (,) ) )
147120, 140, 141, 142, 144, 114, 52, 146dvmptres 22492 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  t ) )  =  ( t  e.  ( 0 (,) 1 )  |->  1 ) )
148120, 136, 138, 147, 15dvmptcmul 22493 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( Y  x.  t ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( Y  x.  1 ) ) )
14915mulid1d 9630 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Y  x.  1 )  =  Y )
150149mpteq2dv 4544 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 (,) 1 ) 
|->  ( Y  x.  1 ) )  =  ( t  e.  ( 0 (,) 1 )  |->  Y ) )
151148, 150eqtrd 2498 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( Y  x.  t ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  Y ) )
15224adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  Z  e.  CC )
153124, 28sylan2 474 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  (
1  -  t )  e.  CC )
154152, 153mulcld 9633 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( Z  x.  ( 1  -  t ) )  e.  CC )
155 negex 9837 . . . . . . . . . . 11  |-  -u Z  e.  _V
156155a1i 11 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  -u Z  e.  _V )
157 negex 9837 . . . . . . . . . . . . 13  |-  -u 1  e.  _V
158157a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  -u 1  e.  _V )
159 1cnd 9629 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  1  e.  CC )
160 0red 9614 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  0  e.  RR )
161 1cnd 9629 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  RR )  ->  1  e.  CC )
162 0red 9614 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  RR )  ->  0  e.  RR )
163 1cnd 9629 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
1  e.  CC )
164120, 163dvmptc 22487 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  RR  |->  1 ) )  =  ( t  e.  RR  |->  0 ) )
165120, 161, 162, 164, 144, 114, 52, 146dvmptres 22492 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  1 ) )  =  ( t  e.  ( 0 (,) 1 )  |->  0 ) )
166120, 159, 160, 165, 136, 138, 147dvmptsub 22496 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( 1  -  t ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( 0  -  1 ) ) )
167 df-neg 9827 . . . . . . . . . . . . . 14  |-  -u 1  =  ( 0  -  1 )
168167mpteq2i 4540 . . . . . . . . . . . . 13  |-  ( t  e.  ( 0 (,) 1 )  |->  -u 1
)  =  ( t  e.  ( 0 (,) 1 )  |->  ( 0  -  1 ) )
169166, 168syl6eqr 2516 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( 1  -  t ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  -u
1 ) )
170120, 153, 158, 169, 24dvmptcmul 22493 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( Z  x.  ( 1  -  t ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( Z  x.  -u 1
) ) )
171 neg1cn 10660 . . . . . . . . . . . . . 14  |-  -u 1  e.  CC
172 mulcom 9595 . . . . . . . . . . . . . 14  |-  ( ( Z  e.  CC  /\  -u 1  e.  CC )  ->  ( Z  x.  -u 1 )  =  (
-u 1  x.  Z
) )
17324, 171, 172sylancl 662 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Z  x.  -u 1
)  =  ( -u
1  x.  Z ) )
17424mulm1d 10029 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( -u 1  x.  Z
)  =  -u Z
)
175173, 174eqtrd 2498 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Z  x.  -u 1
)  =  -u Z
)
176175mpteq2dv 4544 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 (,) 1 ) 
|->  ( Z  x.  -u 1
) )  =  ( t  e.  ( 0 (,) 1 )  |->  -u Z ) )
177170, 176eqtrd 2498 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( Z  x.  ( 1  -  t ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  -u Z ) )
178120, 137, 135, 151, 154, 156, 177dvmptadd 22489 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( Y  +  -u Z
) ) )
17915, 24negsubd 9956 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Y  +  -u Z )  =  ( Y  -  Z ) )
180179mpteq2dv 4544 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( t  e.  ( 0 (,) 1 ) 
|->  ( Y  +  -u Z ) )  =  ( t  e.  ( 0 (,) 1 ) 
|->  ( Y  -  Z
) ) )
181178, 180eqtrd 2498 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( Y  -  Z ) ) )
1829adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  X  C_  CC )
18377, 130, 182, 13, 85syl22anc 1229 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( CC  _D  ( F  |`  B ) )  =  ( ( CC 
_D  F )  |`  ( ( int `  ( TopOpen
` fld
) ) `  B
) ) )
18494adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( int `  ( TopOpen
` fld
) ) `  B
)  =  B )
185184reseq2d 5283 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( CC  _D  F )  |`  (
( int `  ( TopOpen
` fld
) ) `  B
) )  =  ( ( CC  _D  F
)  |`  B ) )
186183, 185eqtrd 2498 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( CC  _D  ( F  |`  B ) )  =  ( ( CC 
_D  F )  |`  B ) )
18747oveq2d 6312 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( CC  _D  ( F  |`  B ) )  =  ( CC  _D  ( z  e.  B  |->  ( F `  z
) ) ) )
188 dvfcn 22438 . . . . . . . . . . . . 13  |-  ( CC 
_D  ( F  |`  B ) ) : dom  ( CC  _D  ( F  |`  B ) ) --> CC
189103feq2d 5724 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( CC  _D  ( F  |`  B ) ) : dom  ( CC  _D  ( F  |`  B ) ) --> CC  <->  ( CC  _D  ( F  |`  B ) ) : B --> CC ) )
190188, 189mpbii 211 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( CC  _D  ( F  |`  B ) ) : B --> CC )
191186feq1d 5723 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( CC  _D  ( F  |`  B ) ) : B --> CC  <->  ( ( CC  _D  F )  |`  B ) : B --> CC ) )
192190, 191mpbid 210 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( CC  _D  F )  |`  B ) : B --> CC )
193192feqmptd 5926 . . . . . . . . . 10  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( CC  _D  F )  |`  B )  =  ( z  e.  B  |->  ( ( ( CC  _D  F )  |`  B ) `  z
) ) )
194 fvres 5886 . . . . . . . . . . 11  |-  ( z  e.  B  ->  (
( ( CC  _D  F )  |`  B ) `
 z )  =  ( ( CC  _D  F ) `  z
) )
195194mpteq2ia 4539 . . . . . . . . . 10  |-  ( z  e.  B  |->  ( ( ( CC  _D  F
)  |`  B ) `  z ) )  =  ( z  e.  B  |->  ( ( CC  _D  F ) `  z
) )
196193, 195syl6eq 2514 . . . . . . . . 9  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( CC  _D  F )  |`  B )  =  ( z  e.  B  |->  ( ( CC 
_D  F ) `  z ) ) )
197186, 187, 1963eqtr3d 2506 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( CC  _D  (
z  e.  B  |->  ( F `  z ) ) )  =  ( z  e.  B  |->  ( ( CC  _D  F
) `  z )
) )
198 fveq2 5872 . . . . . . . 8  |-  ( z  =  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) )  ->  (
( CC  _D  F
) `  z )  =  ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )
199120, 122, 125, 127, 132, 134, 181, 197, 48, 198dvmptco 22501 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 (,) 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( ( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z ) ) ) )
200118, 199eqtrd 2498 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )  =  ( t  e.  ( 0 (,) 1 )  |->  ( ( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z ) ) ) )
201200dmeqd 5215 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  dom  ( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )  =  dom  ( t  e.  ( 0 (,) 1 ) 
|->  ( ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z )
) ) )
202 ovex 6324 . . . . . . 7  |-  ( ( ( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  x.  ( Y  -  Z ) )  e. 
_V
203202rgenw 2818 . . . . . 6  |-  A. t  e.  ( 0 (,) 1
) ( ( ( CC  _D  F ) `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )  x.  ( Y  -  Z
) )  e.  _V
204 dmmptg 5510 . . . . . 6  |-  ( A. t  e.  ( 0 (,) 1 ) ( ( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z ) )  e.  _V  ->  dom  ( t  e.  ( 0 (,) 1 ) 
|->  ( ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z )
) )  =  ( 0 (,) 1 ) )
205203, 204mp1i 12 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  dom  ( t  e.  ( 0 (,) 1 ) 
|->  ( ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z )
) )  =  ( 0 (,) 1 ) )
206201, 205eqtrd 2498 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  dom  ( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )  =  ( 0 (,) 1 ) )
207 dvlipcn.m . . . . . 6  |-  ( ph  ->  M  e.  RR )
208207adantr 465 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  M  e.  RR )
209126abscld 13279 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( abs `  ( Y  -  Z )
)  e.  RR )
210208, 209remulcld 9641 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( M  x.  ( abs `  ( Y  -  Z ) ) )  e.  RR )
211200fveq1d 5874 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( RR  _D  ( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `  t )  =  ( ( t  e.  ( 0 (,) 1 ) 
|->  ( ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z )
) ) `  t
) )
212 eqid 2457 . . . . . . . . . . . . 13  |-  ( t  e.  ( 0 (,) 1 )  |->  ( ( ( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  x.  ( Y  -  Z ) ) )  =  ( t  e.  ( 0 (,) 1
)  |->  ( ( ( CC  _D  F ) `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )  x.  ( Y  -  Z
) ) )
213212fvmpt2 5964 . . . . . . . . . . . 12  |-  ( ( t  e.  ( 0 (,) 1 )  /\  ( ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z )
)  e.  _V )  ->  ( ( t  e.  ( 0 (,) 1
)  |->  ( ( ( CC  _D  F ) `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )  x.  ( Y  -  Z
) ) ) `  t )  =  ( ( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z ) ) )
214202, 213mpan2 671 . . . . . . . . . . 11  |-  ( t  e.  ( 0 (,) 1 )  ->  (
( t  e.  ( 0 (,) 1 ) 
|->  ( ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z )
) ) `  t
)  =  ( ( ( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  x.  ( Y  -  Z ) ) )
215211, 214sylan9eq 2518 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  t
)  =  ( ( ( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  x.  ( Y  -  Z ) ) )
216215fveq2d 5876 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `
 t ) )  =  ( abs `  (
( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) )  x.  ( Y  -  Z ) ) ) )
217 dvfcn 22438 . . . . . . . . . . 11  |-  ( CC 
_D  F ) : dom  ( CC  _D  F ) --> CC
2185ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  B  C_ 
dom  ( CC  _D  F ) )
219218, 125sseldd 3500 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  e.  dom  ( CC 
_D  F ) )
220 ffvelrn 6030 . . . . . . . . . . 11  |-  ( ( ( CC  _D  F
) : dom  ( CC  _D  F ) --> CC 
/\  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) )  e.  dom  ( CC  _D  F
) )  ->  (
( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  e.  CC )
221217, 219, 220sylancr 663 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  (
( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  e.  CC )
222221, 127absmuld 13297 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( ( CC  _D  F ) `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) )  x.  ( Y  -  Z
) ) )  =  ( ( abs `  (
( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) )  x.  ( abs `  ( Y  -  Z
) ) ) )
223216, 222eqtrd 2498 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `
 t ) )  =  ( ( abs `  ( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  x.  ( abs `  ( Y  -  Z ) ) ) )
224221abscld 13279 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )  e.  RR )
225207ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  M  e.  RR )
226127abscld 13279 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( Y  -  Z ) )  e.  RR )
227127absge0d 13287 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  0  <_  ( abs `  ( Y  -  Z )
) )
228 dvlipcn.l . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  B )  ->  ( abs `  ( ( CC 
_D  F ) `  x ) )  <_  M )
229228ralrimiva 2871 . . . . . . . . . . . 12  |-  ( ph  ->  A. x  e.  B  ( abs `  ( ( CC  _D  F ) `
 x ) )  <_  M )
230 fveq2 5872 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  (
( CC  _D  F
) `  x )  =  ( ( CC 
_D  F ) `  y ) )
231230fveq2d 5876 . . . . . . . . . . . . . 14  |-  ( x  =  y  ->  ( abs `  ( ( CC 
_D  F ) `  x ) )  =  ( abs `  (
( CC  _D  F
) `  y )
) )
232231breq1d 4466 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( abs `  (
( CC  _D  F
) `  x )
)  <_  M  <->  ( abs `  ( ( CC  _D  F ) `  y
) )  <_  M
) )
233232cbvralv 3084 . . . . . . . . . . . 12  |-  ( A. x  e.  B  ( abs `  ( ( CC 
_D  F ) `  x ) )  <_  M 
<-> 
A. y  e.  B  ( abs `  ( ( CC  _D  F ) `
 y ) )  <_  M )
234229, 233sylib 196 . . . . . . . . . . 11  |-  ( ph  ->  A. y  e.  B  ( abs `  ( ( CC  _D  F ) `
 y ) )  <_  M )
235234ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  A. y  e.  B  ( abs `  ( ( CC  _D  F ) `  y
) )  <_  M
)
236 fveq2 5872 . . . . . . . . . . . . 13  |-  ( y  =  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) )  ->  (
( CC  _D  F
) `  y )  =  ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )
237236fveq2d 5876 . . . . . . . . . . . 12  |-  ( y  =  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) )  ->  ( abs `  ( ( CC 
_D  F ) `  y ) )  =  ( abs `  (
( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )
238237breq1d 4466 . . . . . . . . . . 11  |-  ( y  =  ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) )  ->  (
( abs `  (
( CC  _D  F
) `  y )
)  <_  M  <->  ( abs `  ( ( CC  _D  F ) `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )  <_  M
) )
239238rspcv 3206 . . . . . . . . . 10  |-  ( ( ( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  e.  B  ->  ( A. y  e.  B  ( abs `  ( ( CC  _D  F ) `
 y ) )  <_  M  ->  ( abs `  ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )  <_  M ) )
240125, 235, 239sylc 60 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( CC 
_D  F ) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )  <_  M )
241224, 225, 226, 227, 240lemul1ad 10505 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  (
( abs `  (
( CC  _D  F
) `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) )  x.  ( abs `  ( Y  -  Z
) ) )  <_ 
( M  x.  ( abs `  ( Y  -  Z ) ) ) )
242223, 241eqbrtrd 4476 . . . . . . 7  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  t  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `
 t ) )  <_  ( M  x.  ( abs `  ( Y  -  Z ) ) ) )
243242ralrimiva 2871 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  A. t  e.  (
0 (,) 1 ) ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  t
) )  <_  ( M  x.  ( abs `  ( Y  -  Z
) ) ) )
244 nfv 1708 . . . . . . 7  |-  F/ z ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  t
) )  <_  ( M  x.  ( abs `  ( Y  -  Z
) ) )
245 nfcv 2619 . . . . . . . . 9  |-  F/_ t abs
246 nfcv 2619 . . . . . . . . . . 11  |-  F/_ t RR
247 nfcv 2619 . . . . . . . . . . 11  |-  F/_ t  _D
248 nfmpt1 4546 . . . . . . . . . . 11  |-  F/_ t
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) )
249246, 247, 248nfov 6322 . . . . . . . . . 10  |-  F/_ t
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) )
250 nfcv 2619 . . . . . . . . . 10  |-  F/_ t
z
251249, 250nffv 5879 . . . . . . . . 9  |-  F/_ t
( ( RR  _D  ( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `  z )
252245, 251nffv 5879 . . . . . . . 8  |-  F/_ t
( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  z
) )
253 nfcv 2619 . . . . . . . 8  |-  F/_ t  <_
254 nfcv 2619 . . . . . . . 8  |-  F/_ t
( M  x.  ( abs `  ( Y  -  Z ) ) )
255252, 253, 254nfbr 4500 . . . . . . 7  |-  F/ t ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  z
) )  <_  ( M  x.  ( abs `  ( Y  -  Z
) ) )
256 fveq2 5872 . . . . . . . . 9  |-  ( t  =  z  ->  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  t
)  =  ( ( RR  _D  ( t  e.  ( 0 [,] 1 )  |->  ( F `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) ) ) ) `  z ) )
257256fveq2d 5876 . . . . . . . 8  |-  ( t  =  z  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `
 t ) )  =  ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  z
) ) )
258257breq1d 4466 . . . . . . 7  |-  ( t  =  z  ->  (
( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  t
) )  <_  ( M  x.  ( abs `  ( Y  -  Z
) ) )  <->  ( abs `  ( ( RR  _D  ( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `  z ) )  <_ 
( M  x.  ( abs `  ( Y  -  Z ) ) ) ) )
259244, 255, 258cbvral 3080 . . . . . 6  |-  ( A. t  e.  ( 0 (,) 1 ) ( abs `  ( ( RR  _D  ( t  e.  ( 0 [,] 1 )  |->  ( F `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) ) ) ) `  t ) )  <_  ( M  x.  ( abs `  ( Y  -  Z )
) )  <->  A. z  e.  ( 0 (,) 1
) ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  z
) )  <_  ( M  x.  ( abs `  ( Y  -  Z
) ) ) )
260243, 259sylib 196 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  ->  A. z  e.  (
0 (,) 1 ) ( abs `  (
( RR  _D  (
t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) ) `  z
) )  <_  ( M  x.  ( abs `  ( Y  -  Z
) ) ) )
261260r19.21bi 2826 . . . 4  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  z  e.  ( 0 (,) 1
) )  ->  ( abs `  ( ( RR 
_D  ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ) `
 z ) )  <_  ( M  x.  ( abs `  ( Y  -  Z ) ) ) )
2623, 4, 107, 206, 210, 261dvlip 22520 . . 3  |-  ( ( ( ph  /\  ( Y  e.  B  /\  Z  e.  B )
)  /\  ( 1  e.  ( 0 [,] 1 )  /\  0  e.  ( 0 [,] 1
) ) )  -> 
( abs `  (
( ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ` 
1 )  -  (
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) `  0
) ) )  <_ 
( ( M  x.  ( abs `  ( Y  -  Z ) ) )  x.  ( abs `  ( 1  -  0 ) ) ) )
2631, 2, 262mpanr12 685 . 2  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( abs `  (
( ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ` 
1 )  -  (
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) `  0
) ) )  <_ 
( ( M  x.  ( abs `  ( Y  -  Z ) ) )  x.  ( abs `  ( 1  -  0 ) ) ) )
264 oveq2 6304 . . . . . . . . 9  |-  ( t  =  1  ->  ( Y  x.  t )  =  ( Y  x.  1 ) )
265 oveq2 6304 . . . . . . . . . . 11  |-  ( t  =  1  ->  (
1  -  t )  =  ( 1  -  1 ) )
266 1m1e0 10625 . . . . . . . . . . 11  |-  ( 1  -  1 )  =  0
267265, 266syl6eq 2514 . . . . . . . . . 10  |-  ( t  =  1  ->  (
1  -  t )  =  0 )
268267oveq2d 6312 . . . . . . . . 9  |-  ( t  =  1  ->  ( Z  x.  ( 1  -  t ) )  =  ( Z  x.  0 ) )
269264, 268oveq12d 6314 . . . . . . . 8  |-  ( t  =  1  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  =  ( ( Y  x.  1 )  +  ( Z  x.  0 ) ) )
270269fveq2d 5876 . . . . . . 7  |-  ( t  =  1  ->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  =  ( F `  ( ( Y  x.  1 )  +  ( Z  x.  0 ) ) ) )
271 eqid 2457 . . . . . . 7  |-  ( t  e.  ( 0 [,] 1 )  |->  ( F `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) ) )  =  ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) )
272 fvex 5882 . . . . . . 7  |-  ( F `
 ( ( Y  x.  1 )  +  ( Z  x.  0 ) ) )  e. 
_V
273270, 271, 272fvmpt 5956 . . . . . 6  |-  ( 1  e.  ( 0 [,] 1 )  ->  (
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) `  1
)  =  ( F `
 ( ( Y  x.  1 )  +  ( Z  x.  0 ) ) ) )
2741, 273ax-mp 5 . . . . 5  |-  ( ( t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) `  1 )  =  ( F `  ( ( Y  x.  1 )  +  ( Z  x.  0 ) ) )
27524mul01d 9796 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Z  x.  0 )  =  0 )
276149, 275oveq12d 6314 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( Y  x.  1 )  +  ( Z  x.  0 ) )  =  ( Y  +  0 ) )
27715addid1d 9797 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Y  +  0 )  =  Y )
278276, 277eqtrd 2498 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( Y  x.  1 )  +  ( Z  x.  0 ) )  =  Y )
279278fveq2d 5876 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( F `  (
( Y  x.  1 )  +  ( Z  x.  0 ) ) )  =  ( F `
 Y ) )
280274, 279syl5eq 2510 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ` 
1 )  =  ( F `  Y ) )
281 oveq2 6304 . . . . . . . . 9  |-  ( t  =  0  ->  ( Y  x.  t )  =  ( Y  x.  0 ) )
282 oveq2 6304 . . . . . . . . . . 11  |-  ( t  =  0  ->  (
1  -  t )  =  ( 1  -  0 ) )
283 1m0e1 10667 . . . . . . . . . . 11  |-  ( 1  -  0 )  =  1
284282, 283syl6eq 2514 . . . . . . . . . 10  |-  ( t  =  0  ->  (
1  -  t )  =  1 )
285284oveq2d 6312 . . . . . . . . 9  |-  ( t  =  0  ->  ( Z  x.  ( 1  -  t ) )  =  ( Z  x.  1 ) )
286281, 285oveq12d 6314 . . . . . . . 8  |-  ( t  =  0  ->  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) )  =  ( ( Y  x.  0 )  +  ( Z  x.  1 ) ) )
287286fveq2d 5876 . . . . . . 7  |-  ( t  =  0  ->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) )  =  ( F `  ( ( Y  x.  0 )  +  ( Z  x.  1 ) ) ) )
288 fvex 5882 . . . . . . 7  |-  ( F `
 ( ( Y  x.  0 )  +  ( Z  x.  1 ) ) )  e. 
_V
289287, 271, 288fvmpt 5956 . . . . . 6  |-  ( 0  e.  ( 0 [,] 1 )  ->  (
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) `  0
)  =  ( F `
 ( ( Y  x.  0 )  +  ( Z  x.  1 ) ) ) )
2902, 289ax-mp 5 . . . . 5  |-  ( ( t  e.  ( 0 [,] 1 )  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t
) ) ) ) ) `  0 )  =  ( F `  ( ( Y  x.  0 )  +  ( Z  x.  1 ) ) )
29115mul01d 9796 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Y  x.  0 )  =  0 )
29224mulid1d 9630 . . . . . . . 8  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( Z  x.  1 )  =  Z )
293291, 292oveq12d 6314 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( Y  x.  0 )  +  ( Z  x.  1 ) )  =  ( 0  +  Z ) )
29424addid2d 9798 . . . . . . 7  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( 0  +  Z
)  =  Z )
295293, 294eqtrd 2498 . . . . . 6  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( Y  x.  0 )  +  ( Z  x.  1 ) )  =  Z )
296295fveq2d 5876 . . . . 5  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( F `  (
( Y  x.  0 )  +  ( Z  x.  1 ) ) )  =  ( F `
 Z ) )
297290, 296syl5eq 2510 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ` 
0 )  =  ( F `  Z ) )
298280, 297oveq12d 6314 . . 3  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( ( t  e.  ( 0 [,] 1 )  |->  ( F `
 ( ( Y  x.  t )  +  ( Z  x.  (
1  -  t ) ) ) ) ) `
 1 )  -  ( ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ` 
0 ) )  =  ( ( F `  Y )  -  ( F `  Z )
) )
299298fveq2d 5876 . 2  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( abs `  (
( ( t  e.  ( 0 [,] 1
)  |->  ( F `  ( ( Y  x.  t )  +  ( Z  x.  ( 1  -  t ) ) ) ) ) ` 
1 )  -  (
( t  e.  ( 0 [,] 1 ) 
|->  ( F `  (
( Y  x.  t
)  +  ( Z  x.  ( 1  -  t ) ) ) ) ) `  0
) ) )  =  ( abs `  (
( F `  Y
)  -  ( F `
 Z ) ) ) )
300283fveq2i 5875 . . . . 5  |-  ( abs `  ( 1  -  0 ) )  =  ( abs `  1 )
301 abs1 13142 . . . . 5  |-  ( abs `  1 )  =  1
302300, 301eqtri 2486 . . . 4  |-  ( abs `  ( 1  -  0 ) )  =  1
303302oveq2i 6307 . . 3  |-  ( ( M  x.  ( abs `  ( Y  -  Z
) ) )  x.  ( abs `  (
1  -  0 ) ) )  =  ( ( M  x.  ( abs `  ( Y  -  Z ) ) )  x.  1 )
304210recnd 9639 . . . 4  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( M  x.  ( abs `  ( Y  -  Z ) ) )  e.  CC )
305304mulid1d 9630 . . 3  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( M  x.  ( abs `  ( Y  -  Z ) ) )  x.  1 )  =  ( M  x.  ( abs `  ( Y  -  Z ) ) ) )
306303, 305syl5eq 2510 . 2  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( ( M  x.  ( abs `  ( Y  -  Z ) ) )  x.  ( abs `  ( 1  -  0 ) ) )  =  ( M  x.  ( abs `  ( Y  -  Z ) ) ) )
307263, 299, 3063brtr3d 4485 1  |-  ( (
ph  /\  ( Y  e.  B  /\  Z  e.  B ) )  -> 
( abs `  (
( F `  Y
)  -  ( F `
 Z ) ) )  <_  ( M  x.  ( abs `  ( Y  -  Z )
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1395    e. wcel 1819   A.wral 2807   _Vcvv 3109    i^i cin 3470    C_ wss 3471   {cpr 4034   class class class wbr 4456    |-> cmpt 4515   dom cdm 5008   ran crn 5009    |` cres 5010    o. ccom 5012   -->wf 5590   ` cfv 5594  (class class class)co 6296   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510    + caddc 9512    x. cmul 9514   RR*cxr 9644    <_ cle 9646    - cmin 9824   -ucneg 9825   (,)cioo 11554   [,]cicc 11557   abscabs 13079   ↾t crest 14838   TopOpenctopn 14839   topGenctg 14855   *Metcxmt 18530   ballcbl 18532  ℂfldccnfld 18547   Topctop 19521   intcnt 19645    Cn ccn 19852    tX ctx 20187   -cn->ccncf 21506    _D cdv 22393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-rep 4568  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-inf2 8075  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586  ax-pre-sup 9587  ax-addf 9588  ax-mulf 9589
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-int 4289  df-iun 4334  df-iin 4335  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-se 4848  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-of 6539  df-om 6700  df-1st 6799  df-2nd 6800  df-supp 6918  df-recs 7060  df-rdg 7094  df-1o 7148  df-2o 7149  df-oadd 7152  df-er 7329  df-map 7440  df-pm 7441  df-ixp 7489  df-en 7536  df-dom 7537  df-sdom 7538  df-fin 7539  df-fsupp 7848  df-fi 7889  df-sup 7919  df-oi 7953  df-card 8337  df-cda 8565  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-3 10616  df-4 10617  df-5 10618  df-6 10619  df-7 10620  df-8 10621  df-9 10622  df-10 10623  df-n0 10817  df-z 10886  df-dec 11001  df-uz 11107  df-q 11208  df-rp 11246  df-xneg 11343  df-xadd 11344  df-xmul 11345  df-ioo 11558  df-ico 11560  df-icc 11561  df-fz 11698  df-fzo 11822  df-seq 12111  df-exp 12170  df-hash 12409  df-cj 12944  df-re 12945  df-im 12946  df-sqrt 13080  df-abs 13081  df-struct 14646  df-ndx 14647  df-slot 14648  df-base 14649  df-sets 14650  df-ress 14651  df-plusg 14725  df-mulr 14726  df-starv 14727  df-sca 14728  df-vsca 14729  df-ip 14730  df-tset 14731  df-ple 14732  df-ds 14734  df-unif 14735  df-hom 14736  df-cco 14737  df-rest 14840  df-topn 14841  df-0g 14859  df-gsum 14860  df-topgen 14861  df-pt 14862  df-prds 14865  df-xrs 14919  df-qtop 14924  df-imas 14925  df-xps 14927  df-mre 15003  df-mrc 15004  df-acs 15006  df-mgm 15999  df-sgrp 16038  df-mnd 16048  df-submnd 16094  df-mulg 16187  df-cntz 16482  df-cmn 16927  df-psmet 18538  df-xmet 18539  df-met 18540  df-bl 18541  df-mopn 18542  df-fbas 18543  df-fg 18544  df-cnfld 18548  df-top 19526  df-bases 19528  df-topon 19529  df-topsp 19530  df-cld 19647  df-ntr 19648  df-cls 19649  df-nei 19726  df-lp 19764  df-perf 19765  df-cn 19855  df-cnp 19856  df-haus 19943  df-cmp 20014  df-tx 20189  df-hmeo 20382  df-fil 20473  df-fm 20565  df-flim 20566  df-flf 20567  df-xms 20949  df-ms 20950  df-tms 20951  df-cncf 21508  df-limc 22396  df-dv 22397
This theorem is referenced by:  dvlip2  22522  dv11cn  22528
  Copyright terms: Public domain W3C validator