Metamath Proof Explorer

Theorem dvlipcn

Description: A complex function with derivative bounded by M on an open ball is M-Lipschitz continuous. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses 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 dvlipcn 
|- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )

Proof

Step Hyp Ref Expression
1 dvlipcn.x 
 |-  ( ph -> X C_ CC )
2 dvlipcn.f 
 |-  ( ph -> F : X --> CC )
3 dvlipcn.a 
 |-  ( ph -> A e. CC )
4 dvlipcn.r 
 |-  ( ph -> R e. RR* )
5 dvlipcn.b 
 |-  B = ( A ( ball ` ( abs o. - ) ) R )
6 dvlipcn.d 
 |-  ( ph -> B C_ dom ( CC _D F ) )
7 dvlipcn.m 
 |-  ( ph -> M e. RR )
8 dvlipcn.l 
 |-  ( ( ph /\ x e. B ) -> ( abs ` ( ( CC _D F ) ` x ) ) <_ M )
9 1elunit 
 |-  1 e. ( 0 [,] 1 )
10 0elunit 
 |-  0 e. ( 0 [,] 1 )
11 0red 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> 0 e. RR )
12 1red 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> 1 e. RR )
13 ssidd 
 |-  ( ph -> CC C_ CC )
14 13 2 1 dvbss 
 |-  ( ph -> dom ( CC _D F ) C_ X )
15 6 14 sstrd 
 |-  ( ph -> B C_ X )
16 15 1 sstrd 
 |-  ( ph -> B C_ CC )
17 16 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> B C_ CC )
18 simprl 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Y e. B )
19 17 18 sseldd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Y e. CC )
20 19 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Y e. CC )
21 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
22 ax-resscn 
 |-  RR C_ CC
23 21 22 sstri 
 |-  ( 0 [,] 1 ) C_ CC
24 simpr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> t e. ( 0 [,] 1 ) )
25 23 24 sselid 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> t e. CC )
26 20 25 mulcomd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( Y x. t ) = ( t x. Y ) )
27 simprr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Z e. B )
28 17 27 sseldd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Z e. CC )
29 28 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Z e. CC )
30 iirev 
 |-  ( t e. ( 0 [,] 1 ) -> ( 1 - t ) e. ( 0 [,] 1 ) )
31 30 adantl 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( 1 - t ) e. ( 0 [,] 1 ) )
32 23 31 sselid 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( 1 - t ) e. CC )
33 29 32 mulcomd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( Z x. ( 1 - t ) ) = ( ( 1 - t ) x. Z ) )
34 26 33 oveq12d 
 |-  ( ( ( 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 ) ) )
35 3 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> A e. CC )
36 4 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> R e. RR* )
37 18 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Y e. B )
38 27 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Z e. B )
39 5 blcvx 
 |-  ( ( ( 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 )
40 35 36 37 38 24 39 syl23anc 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. Y ) + ( ( 1 - t ) x. Z ) ) e. B )
41 34 40 eqeltrd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. B )
42 eqidd 
 |-  ( ( 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 ) ) ) ) )
43 2 15 fssresd 
 |-  ( ph -> ( F |` B ) : B --> CC )
44 43 feqmptd 
 |-  ( ph -> ( F |` B ) = ( z e. B |-> ( ( F |` B ) ` z ) ) )
45 fvres 
 |-  ( z e. B -> ( ( F |` B ) ` z ) = ( F ` z ) )
46 45 mpteq2ia 
 |-  ( z e. B |-> ( ( F |` B ) ` z ) ) = ( z e. B |-> ( F ` z ) )
47 44 46 eqtrdi 
 |-  ( ph -> ( F |` B ) = ( z e. B |-> ( F ` z ) ) )
48 47 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F |` B ) = ( z e. B |-> ( F ` z ) ) )
49 fveq2 
 |-  ( z = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( F ` z ) = ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
50 41 42 48 49 fmptco 
 |-  ( ( 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 ) ) ) ) ) )
51 41 fmpttd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) : ( 0 [,] 1 ) --> B )
52 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
53 52 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
54 53 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
55 ssid 
 |-  CC C_ CC
56 cncfmptc 
 |-  ( ( Y e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> Y ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
57 23 55 56 mp3an23 
 |-  ( Y e. CC -> ( t e. ( 0 [,] 1 ) |-> Y ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
58 19 57 syl 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> Y ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
59 cncfmptid 
 |-  ( ( ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
60 23 55 59 mp2an 
 |-  ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC )
61 60 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
62 58 61 mulcncf 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( Y x. t ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
63 cncfmptc 
 |-  ( ( Z e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> Z ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
64 23 55 63 mp3an23 
 |-  ( Z e. CC -> ( t e. ( 0 [,] 1 ) |-> Z ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
65 28 64 syl 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> Z ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
66 52 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
67 66 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
68 ax-1cn 
 |-  1 e. CC
69 cncfmptc 
 |-  ( ( 1 e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
70 68 23 55 69 mp3an 
 |-  ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC )
71 70 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
72 52 67 71 61 cncfmpt2f 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( 1 - t ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
73 65 72 mulcncf 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( Z x. ( 1 - t ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
74 52 54 62 73 cncfmpt2f 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
75 cncffvrn 
 |-  ( ( 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 ) )
76 17 74 75 syl2anc 
 |-  ( ( 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 ) )
77 51 76 mpbird 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> B ) )
78 ssidd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> CC C_ CC )
79 43 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F |` B ) : B --> CC )
80 52 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
81 80 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
82 52 81 dvres 
 |-  ( ( ( CC C_ CC /\ F : X --> CC ) /\ ( X C_ CC /\ B C_ CC ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) )
83 13 2 1 16 82 syl22anc 
 |-  ( ph -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) )
84 52 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
85 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
86 52 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
87 86 blopn 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ R e. RR* ) -> ( A ( ball ` ( abs o. - ) ) R ) e. ( TopOpen ` CCfld ) )
88 85 3 4 87 mp3an2i 
 |-  ( ph -> ( A ( ball ` ( abs o. - ) ) R ) e. ( TopOpen ` CCfld ) )
89 5 88 eqeltrid 
 |-  ( ph -> B e. ( TopOpen ` CCfld ) )
90 isopn3i 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ B e. ( TopOpen ` CCfld ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` B ) = B )
91 84 89 90 sylancr 
 |-  ( ph -> ( ( int ` ( TopOpen ` CCfld ) ) ` B ) = B )
92 91 reseq2d 
 |-  ( ph -> ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) = ( ( CC _D F ) |` B ) )
93 83 92 eqtrd 
 |-  ( ph -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` B ) )
94 93 dmeqd 
 |-  ( ph -> dom ( CC _D ( F |` B ) ) = dom ( ( CC _D F ) |` B ) )
95 dmres 
 |-  dom ( ( CC _D F ) |` B ) = ( B i^i dom ( CC _D F ) )
96 df-ss 
 |-  ( B C_ dom ( CC _D F ) <-> ( B i^i dom ( CC _D F ) ) = B )
97 6 96 sylib 
 |-  ( ph -> ( B i^i dom ( CC _D F ) ) = B )
98 95 97 syl5eq 
 |-  ( ph -> dom ( ( CC _D F ) |` B ) = B )
99 94 98 eqtrd 
 |-  ( ph -> dom ( CC _D ( F |` B ) ) = B )
100 99 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> dom ( CC _D ( F |` B ) ) = B )
101 dvcn 
 |-  ( ( ( CC C_ CC /\ ( F |` B ) : B --> CC /\ B C_ CC ) /\ dom ( CC _D ( F |` B ) ) = B ) -> ( F |` B ) e. ( B -cn-> CC ) )
102 78 79 17 100 101 syl31anc 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F |` B ) e. ( B -cn-> CC ) )
103 77 102 cncfco 
 |-  ( ( 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 ) )
104 50 103 eqeltrrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
105 22 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> RR C_ CC )
106 21 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 [,] 1 ) C_ RR )
107 2 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> F : X --> CC )
108 15 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> B C_ X )
109 108 41 sseldd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. X )
110 107 109 ffvelrnd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. CC )
111 52 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
112 1re 
 |-  1 e. RR
113 iccntr 
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] 1 ) ) = ( 0 (,) 1 ) )
114 11 112 113 sylancl 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] 1 ) ) = ( 0 (,) 1 ) )
115 105 106 110 111 52 114 dvmptntr 
 |-  ( ( 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 ) ) ) ) ) ) )
116 reelprrecn 
 |-  RR e. { RR , CC }
117 116 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> RR e. { RR , CC } )
118 cnelprrecn 
 |-  CC e. { RR , CC }
119 118 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> CC e. { RR , CC } )
120 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
121 120 sseli 
 |-  ( t e. ( 0 (,) 1 ) -> t e. ( 0 [,] 1 ) )
122 121 41 sylan2 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. B )
123 19 28 subcld 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y - Z ) e. CC )
124 123 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( Y - Z ) e. CC )
125 15 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> B C_ X )
126 125 sselda 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. B ) -> z e. X )
127 2 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> F : X --> CC )
128 127 ffvelrnda 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. X ) -> ( F ` z ) e. CC )
129 126 128 syldan 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. B ) -> ( F ` z ) e. CC )
130 fvexd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. B ) -> ( ( CC _D F ) ` z ) e. _V )
131 19 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> Y e. CC )
132 121 25 sylan2 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> t e. CC )
133 131 132 mulcld 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( Y x. t ) e. CC )
134 1red 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 1 e. RR )
135 simpr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> t e. RR )
136 135 recnd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> t e. CC )
137 1red 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> 1 e. RR )
138 117 dvmptid 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
139 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
140 139 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 (,) 1 ) C_ RR )
141 iooretop 
 |-  ( 0 (,) 1 ) e. ( topGen ` ran (,) )
142 141 a1i 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 (,) 1 ) e. ( topGen ` ran (,) ) )
143 117 136 137 138 140 111 52 142 dvmptres 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> t ) ) = ( t e. ( 0 (,) 1 ) |-> 1 ) )
144 117 132 134 143 19 dvmptcmul 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Y x. t ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( Y x. 1 ) ) )
145 19 mulid1d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y x. 1 ) = Y )
146 145 mpteq2dv 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 (,) 1 ) |-> ( Y x. 1 ) ) = ( t e. ( 0 (,) 1 ) |-> Y ) )
147 144 146 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Y x. t ) ) ) = ( t e. ( 0 (,) 1 ) |-> Y ) )
148 28 adantr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> Z e. CC )
149 121 32 sylan2 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( 1 - t ) e. CC )
150 148 149 mulcld 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( Z x. ( 1 - t ) ) e. CC )
151 negex 
 |-  -u Z e. _V
152 151 a1i 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> -u Z e. _V )
153 negex 
 |-  -u 1 e. _V
154 153 a1i 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> -u 1 e. _V )
155 1cnd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 1 e. CC )
156 0red 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 0 e. RR )
157 1cnd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> 1 e. CC )
158 0red 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> 0 e. RR )
159 1cnd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> 1 e. CC )
160 117 159 dvmptc 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. RR |-> 1 ) ) = ( t e. RR |-> 0 ) )
161 117 157 158 160 140 111 52 142 dvmptres 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> 1 ) ) = ( t e. ( 0 (,) 1 ) |-> 0 ) )
162 117 155 156 161 132 134 143 dvmptsub 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( 1 - t ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( 0 - 1 ) ) )
163 df-neg 
 |-  -u 1 = ( 0 - 1 )
164 163 mpteq2i 
 |-  ( t e. ( 0 (,) 1 ) |-> -u 1 ) = ( t e. ( 0 (,) 1 ) |-> ( 0 - 1 ) )
165 162 164 eqtr4di 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( 1 - t ) ) ) = ( t e. ( 0 (,) 1 ) |-> -u 1 ) )
166 117 149 154 165 28 dvmptcmul 
 |-  ( ( 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 ) ) )
167 neg1cn 
 |-  -u 1 e. CC
168 mulcom 
 |-  ( ( Z e. CC /\ -u 1 e. CC ) -> ( Z x. -u 1 ) = ( -u 1 x. Z ) )
169 28 167 168 sylancl 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. -u 1 ) = ( -u 1 x. Z ) )
170 28 mulm1d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( -u 1 x. Z ) = -u Z )
171 169 170 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. -u 1 ) = -u Z )
172 171 mpteq2dv 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 (,) 1 ) |-> ( Z x. -u 1 ) ) = ( t e. ( 0 (,) 1 ) |-> -u Z ) )
173 166 172 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Z x. ( 1 - t ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> -u Z ) )
174 117 133 131 147 150 152 173 dvmptadd 
 |-  ( ( 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 ) ) )
175 19 28 negsubd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y + -u Z ) = ( Y - Z ) )
176 175 mpteq2dv 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 (,) 1 ) |-> ( Y + -u Z ) ) = ( t e. ( 0 (,) 1 ) |-> ( Y - Z ) ) )
177 174 176 eqtrd 
 |-  ( ( 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 ) ) )
178 1 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> X C_ CC )
179 78 127 178 17 82 syl22anc 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) )
180 91 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( int ` ( TopOpen ` CCfld ) ) ` B ) = B )
181 180 reseq2d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` ( ( int ` ( TopOpen ` CCfld ) ) ` B ) ) = ( ( CC _D F ) |` B ) )
182 179 181 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` B ) )
183 48 oveq2d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) = ( CC _D ( z e. B |-> ( F ` z ) ) ) )
184 dvfcn 
 |-  ( CC _D ( F |` B ) ) : dom ( CC _D ( F |` B ) ) --> CC
185 100 feq2d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D ( F |` B ) ) : dom ( CC _D ( F |` B ) ) --> CC <-> ( CC _D ( F |` B ) ) : B --> CC ) )
186 184 185 mpbii 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) : B --> CC )
187 182 feq1d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D ( F |` B ) ) : B --> CC <-> ( ( CC _D F ) |` B ) : B --> CC ) )
188 186 187 mpbid 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` B ) : B --> CC )
189 188 feqmptd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` B ) = ( z e. B |-> ( ( ( CC _D F ) |` B ) ` z ) ) )
190 fvres 
 |-  ( z e. B -> ( ( ( CC _D F ) |` B ) ` z ) = ( ( CC _D F ) ` z ) )
191 190 mpteq2ia 
 |-  ( z e. B |-> ( ( ( CC _D F ) |` B ) ` z ) ) = ( z e. B |-> ( ( CC _D F ) ` z ) )
192 189 191 eqtrdi 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` B ) = ( z e. B |-> ( ( CC _D F ) ` z ) ) )
193 182 183 192 3eqtr3d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( z e. B |-> ( F ` z ) ) ) = ( z e. B |-> ( ( CC _D F ) ` z ) ) )
194 fveq2 
 |-  ( z = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( ( CC _D F ) ` z ) = ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
195 117 119 122 124 129 130 177 193 49 194 dvmptco 
 |-  ( ( 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 ) ) ) )
196 115 195 eqtrd 
 |-  ( ( 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 ) ) ) )
197 196 dmeqd 
 |-  ( ( 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 ) ) ) )
198 ovex 
 |-  ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) e. _V
199 198 rgenw 
 |-  A. t e. ( 0 (,) 1 ) ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) e. _V
200 dmmptg 
 |-  ( 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 ) )
201 199 200 mp1i 
 |-  ( ( 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 ) )
202 197 201 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> dom ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) = ( 0 (,) 1 ) )
203 7 adantr 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> M e. RR )
204 123 abscld 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( Y - Z ) ) e. RR )
205 203 204 remulcld 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( M x. ( abs ` ( Y - Z ) ) ) e. RR )
206 196 fveq1d 
 |-  ( ( 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 ) )
207 eqid 
 |-  ( 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 ) ) )
208 207 fvmpt2 
 |-  ( ( 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 ) ) )
209 198 208 mpan2 
 |-  ( 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 ) ) )
210 206 209 sylan9eq 
 |-  ( ( ( 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 ) ) )
211 210 fveq2d 
 |-  ( ( ( 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 ) ) ) )
212 dvfcn 
 |-  ( CC _D F ) : dom ( CC _D F ) --> CC
213 6 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> B C_ dom ( CC _D F ) )
214 213 122 sseldd 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. dom ( CC _D F ) )
215 ffvelrn 
 |-  ( ( ( 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 )
216 212 214 215 sylancr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. CC )
217 216 124 absmuld 
 |-  ( ( ( 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 ) ) ) )
218 211 217 eqtrd 
 |-  ( ( ( 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 ) ) ) )
219 216 abscld 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) e. RR )
220 7 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> M e. RR )
221 124 abscld 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( Y - Z ) ) e. RR )
222 124 absge0d 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 0 <_ ( abs ` ( Y - Z ) ) )
223 2fveq3 
 |-  ( y = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( abs ` ( ( CC _D F ) ` y ) ) = ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) )
224 223 breq1d 
 |-  ( 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 ) )
225 8 ralrimiva 
 |-  ( ph -> A. x e. B ( abs ` ( ( CC _D F ) ` x ) ) <_ M )
226 2fveq3 
 |-  ( x = y -> ( abs ` ( ( CC _D F ) ` x ) ) = ( abs ` ( ( CC _D F ) ` y ) ) )
227 226 breq1d 
 |-  ( x = y -> ( ( abs ` ( ( CC _D F ) ` x ) ) <_ M <-> ( abs ` ( ( CC _D F ) ` y ) ) <_ M ) )
228 227 cbvralvw 
 |-  ( A. x e. B ( abs ` ( ( CC _D F ) ` x ) ) <_ M <-> A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M )
229 225 228 sylib 
 |-  ( ph -> A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M )
230 229 ad2antrr 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M )
231 224 230 122 rspcdva 
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) <_ M )
232 219 220 221 222 231 lemul1ad 
 |-  ( ( ( 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 ) ) ) )
233 218 232 eqbrtrd 
 |-  ( ( ( 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 ) ) ) )
234 233 ralrimiva 
 |-  ( ( 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 ) ) ) )
235 nfv 
 |-  F/ z ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) <_ ( M x. ( abs ` ( Y - Z ) ) )
236 nfcv 
 |-  F/_ t abs
237 nfcv 
 |-  F/_ t RR
238 nfcv 
 |-  F/_ t _D
239 nfmpt1 
 |-  F/_ t ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
240 237 238 239 nfov 
 |-  F/_ t ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) )
241 nfcv 
 |-  F/_ t z
242 240 241 nffv 
 |-  F/_ t ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z )
243 236 242 nffv 
 |-  F/_ t ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) )
244 nfcv 
 |-  F/_ t <_
245 nfcv 
 |-  F/_ t ( M x. ( abs ` ( Y - Z ) ) )
246 243 244 245 nfbr 
 |-  F/ t ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) <_ ( M x. ( abs ` ( Y - Z ) ) )
247 2fveq3 
 |-  ( 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 ) ) )
248 247 breq1d 
 |-  ( 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 ) ) ) ) )
249 235 246 248 cbvralw 
 |-  ( 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 ) ) ) )
250 234 249 sylib 
 |-  ( ( 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 ) ) ) )
251 250 r19.21bi 
 |-  ( ( ( 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 ) ) ) )
252 11 12 104 202 205 251 dvlip 
 |-  ( ( ( 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 ) ) ) )
253 9 10 252 mpanr12 
 |-  ( ( 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 ) ) ) )
254 oveq2 
 |-  ( t = 1 -> ( Y x. t ) = ( Y x. 1 ) )
255 oveq2 
 |-  ( t = 1 -> ( 1 - t ) = ( 1 - 1 ) )
256 1m1e0 
 |-  ( 1 - 1 ) = 0
257 255 256 eqtrdi 
 |-  ( t = 1 -> ( 1 - t ) = 0 )
258 257 oveq2d 
 |-  ( t = 1 -> ( Z x. ( 1 - t ) ) = ( Z x. 0 ) )
259 254 258 oveq12d 
 |-  ( t = 1 -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) = ( ( Y x. 1 ) + ( Z x. 0 ) ) )
260 259 fveq2d 
 |-  ( t = 1 -> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) = ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) )
261 eqid 
 |-  ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
262 fvex 
 |-  ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) e. _V
263 260 261 262 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) = ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) )
264 9 263 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) = ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) )
265 28 mul01d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. 0 ) = 0 )
266 145 265 oveq12d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 1 ) + ( Z x. 0 ) ) = ( Y + 0 ) )
267 19 addid1d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y + 0 ) = Y )
268 266 267 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 1 ) + ( Z x. 0 ) ) = Y )
269 268 fveq2d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) = ( F ` Y ) )
270 264 269 syl5eq 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) = ( F ` Y ) )
271 oveq2 
 |-  ( t = 0 -> ( Y x. t ) = ( Y x. 0 ) )
272 oveq2 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
273 1m0e1 
 |-  ( 1 - 0 ) = 1
274 272 273 eqtrdi 
 |-  ( t = 0 -> ( 1 - t ) = 1 )
275 274 oveq2d 
 |-  ( t = 0 -> ( Z x. ( 1 - t ) ) = ( Z x. 1 ) )
276 271 275 oveq12d 
 |-  ( t = 0 -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) = ( ( Y x. 0 ) + ( Z x. 1 ) ) )
277 276 fveq2d 
 |-  ( t = 0 -> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) = ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) )
278 fvex 
 |-  ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) e. _V
279 277 261 278 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) = ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) )
280 10 279 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) = ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) )
281 19 mul01d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y x. 0 ) = 0 )
282 28 mulid1d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. 1 ) = Z )
283 281 282 oveq12d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 0 ) + ( Z x. 1 ) ) = ( 0 + Z ) )
284 28 addid2d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 + Z ) = Z )
285 283 284 eqtrd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 0 ) + ( Z x. 1 ) ) = Z )
286 285 fveq2d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) = ( F ` Z ) )
287 280 286 syl5eq 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) = ( F ` Z ) )
288 270 287 oveq12d 
 |-  ( ( 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 ) ) )
289 288 fveq2d 
 |-  ( ( 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 ) ) ) )
290 273 fveq2i 
 |-  ( abs ` ( 1 - 0 ) ) = ( abs ` 1 )
291 abs1 
 |-  ( abs ` 1 ) = 1
292 290 291 eqtri 
 |-  ( abs ` ( 1 - 0 ) ) = 1
293 292 oveq2i 
 |-  ( ( M x. ( abs ` ( Y - Z ) ) ) x. ( abs ` ( 1 - 0 ) ) ) = ( ( M x. ( abs ` ( Y - Z ) ) ) x. 1 )
294 205 recnd 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( M x. ( abs ` ( Y - Z ) ) ) e. CC )
295 294 mulid1d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( M x. ( abs ` ( Y - Z ) ) ) x. 1 ) = ( M x. ( abs ` ( Y - Z ) ) ) )
296 293 295 syl5eq 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( M x. ( abs ` ( Y - Z ) ) ) x. ( abs ` ( 1 - 0 ) ) ) = ( M x. ( abs ` ( Y - Z ) ) ) )
297 253 289 296 3brtr3d 
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )