Metamath Proof Explorer

Theorem c1lip3

Description: C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses c1lip3.a 
|- ( ph -> A e. RR )
c1lip3.b 
|- ( ph -> B e. RR )
c1lip3.f 
|- ( ph -> ( F |` RR ) e. ( ( C^n ` RR ) ` 1 ) )
c1lip3.rn 
|- ( ph -> ( F " RR ) C_ RR )
c1lip3.dm 
|- ( ph -> ( A [,] B ) C_ dom F )
Assertion c1lip3 
|- ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )

Proof

Step Hyp Ref Expression
1 c1lip3.a 
 |-  ( ph -> A e. RR )
2 c1lip3.b 
 |-  ( ph -> B e. RR )
3 c1lip3.f 
 |-  ( ph -> ( F |` RR ) e. ( ( C^n ` RR ) ` 1 ) )
4 c1lip3.rn 
 |-  ( ph -> ( F " RR ) C_ RR )
5 c1lip3.dm 
 |-  ( ph -> ( A [,] B ) C_ dom F )
6 df-ima 
 |-  ( F " RR ) = ran ( F |` RR )
7 6 4 eqsstrrid 
 |-  ( ph -> ran ( F |` RR ) C_ RR )
8 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
9 1 2 8 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
10 9 5 ssind 
 |-  ( ph -> ( A [,] B ) C_ ( RR i^i dom F ) )
11 dmres 
 |-  dom ( F |` RR ) = ( RR i^i dom F )
12 10 11 sseqtrrdi 
 |-  ( ph -> ( A [,] B ) C_ dom ( F |` RR ) )
13 1 2 3 7 12 c1lip2 
 |-  ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
14 9 sseld 
 |-  ( ph -> ( x e. ( A [,] B ) -> x e. RR ) )
15 9 sseld 
 |-  ( ph -> ( y e. ( A [,] B ) -> y e. RR ) )
16 14 15 anim12d 
 |-  ( ph -> ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( x e. RR /\ y e. RR ) ) )
17 16 imp 
 |-  ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x e. RR /\ y e. RR ) )
18 fvres 
 |-  ( y e. RR -> ( ( F |` RR ) ` y ) = ( F ` y ) )
19 fvres 
 |-  ( x e. RR -> ( ( F |` RR ) ` x ) = ( F ` x ) )
20 18 19 oveqan12rd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) = ( ( F ` y ) - ( F ` x ) ) )
21 20 fveq2d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) = ( abs ` ( ( F ` y ) - ( F ` x ) ) ) )
22 21 breq1d 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) <-> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
23 22 biimpd 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
24 17 23 syl 
 |-  ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
25 24 ralimdvva 
 |-  ( ph -> ( A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
26 25 reximdv 
 |-  ( ph -> ( E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( ( F |` RR ) ` y ) - ( ( F |` RR ) ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
27 13 26 mpd 
 |-  ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )