Metamath Proof Explorer


Theorem dvlip2

Description: Combine the results of dvlip and dvlipcn into one. (Contributed by Mario Carneiro, 18-Mar-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses dvlip2.s
|- ( ph -> S e. { RR , CC } )
dvlip2.j
|- J = ( ( abs o. - ) |` ( S X. S ) )
dvlip2.x
|- ( ph -> X C_ S )
dvlip2.f
|- ( ph -> F : X --> CC )
dvlip2.a
|- ( ph -> A e. S )
dvlip2.r
|- ( ph -> R e. RR* )
dvlip2.b
|- B = ( A ( ball ` J ) R )
dvlip2.d
|- ( ph -> B C_ dom ( S _D F ) )
dvlip2.m
|- ( ph -> M e. RR )
dvlip2.l
|- ( ( ph /\ x e. B ) -> ( abs ` ( ( S _D F ) ` x ) ) <_ M )
Assertion dvlip2
|- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )

Proof

Step Hyp Ref Expression
1 dvlip2.s
 |-  ( ph -> S e. { RR , CC } )
2 dvlip2.j
 |-  J = ( ( abs o. - ) |` ( S X. S ) )
3 dvlip2.x
 |-  ( ph -> X C_ S )
4 dvlip2.f
 |-  ( ph -> F : X --> CC )
5 dvlip2.a
 |-  ( ph -> A e. S )
6 dvlip2.r
 |-  ( ph -> R e. RR* )
7 dvlip2.b
 |-  B = ( A ( ball ` J ) R )
8 dvlip2.d
 |-  ( ph -> B C_ dom ( S _D F ) )
9 dvlip2.m
 |-  ( ph -> M e. RR )
10 dvlip2.l
 |-  ( ( ph /\ x e. B ) -> ( abs ` ( ( S _D F ) ` x ) ) <_ M )
11 cnxmet
 |-  ( abs o. - ) e. ( *Met ` CC )
12 recnprss
 |-  ( S e. { RR , CC } -> S C_ CC )
13 1 12 syl
 |-  ( ph -> S C_ CC )
14 xmetres2
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ S C_ CC ) -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
15 11 13 14 sylancr
 |-  ( ph -> ( ( abs o. - ) |` ( S X. S ) ) e. ( *Met ` S ) )
16 2 15 eqeltrid
 |-  ( ph -> J e. ( *Met ` S ) )
17 16 ad2antrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> J e. ( *Met ` S ) )
18 5 ad2antrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> A e. S )
19 simplrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Z e. B )
20 19 7 eleqtrdi
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Z e. ( A ( ball ` J ) R ) )
21 6 ad2antrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> R e. RR* )
22 elbl
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ R e. RR* ) -> ( Z e. ( A ( ball ` J ) R ) <-> ( Z e. S /\ ( A J Z ) < R ) ) )
23 17 18 21 22 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Z e. ( A ( ball ` J ) R ) <-> ( Z e. S /\ ( A J Z ) < R ) ) )
24 20 23 mpbid
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Z e. S /\ ( A J Z ) < R ) )
25 24 simpld
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Z e. S )
26 xmetcl
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ Z e. S ) -> ( A J Z ) e. RR* )
27 17 18 25 26 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Z ) e. RR* )
28 simplrl
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Y e. B )
29 28 7 eleqtrdi
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Y e. ( A ( ball ` J ) R ) )
30 elbl
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ R e. RR* ) -> ( Y e. ( A ( ball ` J ) R ) <-> ( Y e. S /\ ( A J Y ) < R ) ) )
31 17 18 21 30 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Y e. ( A ( ball ` J ) R ) <-> ( Y e. S /\ ( A J Y ) < R ) ) )
32 29 31 mpbid
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Y e. S /\ ( A J Y ) < R ) )
33 32 simpld
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Y e. S )
34 xmetcl
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ Y e. S ) -> ( A J Y ) e. RR* )
35 17 18 33 34 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Y ) e. RR* )
36 27 35 ifcld
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) e. RR* )
37 24 simprd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Z ) < R )
38 32 simprd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Y ) < R )
39 breq1
 |-  ( ( A J Z ) = if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) -> ( ( A J Z ) < R <-> if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < R ) )
40 breq1
 |-  ( ( A J Y ) = if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) -> ( ( A J Y ) < R <-> if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < R ) )
41 39 40 ifboth
 |-  ( ( ( A J Z ) < R /\ ( A J Y ) < R ) -> if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < R )
42 37 38 41 syl2anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < R )
43 qbtwnxr
 |-  ( ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) e. RR* /\ R e. RR* /\ if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < R ) -> E. r e. QQ ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r /\ r < R ) )
44 36 21 42 43 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> E. r e. QQ ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r /\ r < R ) )
45 qre
 |-  ( r e. QQ -> r e. RR )
46 rexr
 |-  ( r e. RR -> r e. RR* )
47 xrmaxlt
 |-  ( ( ( A J Y ) e. RR* /\ ( A J Z ) e. RR* /\ r e. RR* ) -> ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r <-> ( ( A J Y ) < r /\ ( A J Z ) < r ) ) )
48 35 27 46 47 syl2an3an
 |-  ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) -> ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r <-> ( ( A J Y ) < r /\ ( A J Z ) < r ) ) )
49 ioossicc
 |-  ( ( A - r ) (,) ( A + r ) ) C_ ( ( A - r ) [,] ( A + r ) )
50 simpr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> S = RR )
51 33 50 eleqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Y e. RR )
52 51 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Y e. RR )
53 xmetsym
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ Y e. S ) -> ( A J Y ) = ( Y J A ) )
54 17 18 33 53 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Y ) = ( Y J A ) )
55 50 sqxpeqd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( S X. S ) = ( RR X. RR ) )
56 55 reseq2d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( RR X. RR ) ) )
57 2 56 eqtrid
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> J = ( ( abs o. - ) |` ( RR X. RR ) ) )
58 57 oveqd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Y J A ) = ( Y ( ( abs o. - ) |` ( RR X. RR ) ) A ) )
59 18 50 eleqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> A e. RR )
60 eqid
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
61 60 remetdval
 |-  ( ( Y e. RR /\ A e. RR ) -> ( Y ( ( abs o. - ) |` ( RR X. RR ) ) A ) = ( abs ` ( Y - A ) ) )
62 51 59 61 syl2anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Y ( ( abs o. - ) |` ( RR X. RR ) ) A ) = ( abs ` ( Y - A ) ) )
63 54 58 62 3eqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Y ) = ( abs ` ( Y - A ) ) )
64 63 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A J Y ) = ( abs ` ( Y - A ) ) )
65 simprll
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A J Y ) < r )
66 64 65 eqbrtrrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( abs ` ( Y - A ) ) < r )
67 59 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> A e. RR )
68 simplr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> r e. RR )
69 52 67 68 absdifltd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( abs ` ( Y - A ) ) < r <-> ( ( A - r ) < Y /\ Y < ( A + r ) ) ) )
70 66 69 mpbid
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) < Y /\ Y < ( A + r ) ) )
71 70 simpld
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A - r ) < Y )
72 70 simprd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Y < ( A + r ) )
73 67 68 resubcld
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A - r ) e. RR )
74 73 rexrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A - r ) e. RR* )
75 67 68 readdcld
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A + r ) e. RR )
76 75 rexrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A + r ) e. RR* )
77 elioo2
 |-  ( ( ( A - r ) e. RR* /\ ( A + r ) e. RR* ) -> ( Y e. ( ( A - r ) (,) ( A + r ) ) <-> ( Y e. RR /\ ( A - r ) < Y /\ Y < ( A + r ) ) ) )
78 74 76 77 syl2anc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( Y e. ( ( A - r ) (,) ( A + r ) ) <-> ( Y e. RR /\ ( A - r ) < Y /\ Y < ( A + r ) ) ) )
79 52 71 72 78 mpbir3and
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Y e. ( ( A - r ) (,) ( A + r ) ) )
80 49 79 sselid
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Y e. ( ( A - r ) [,] ( A + r ) ) )
81 80 fvresd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Y ) = ( F ` Y ) )
82 25 50 eleqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> Z e. RR )
83 82 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Z e. RR )
84 xmetsym
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ Z e. S ) -> ( A J Z ) = ( Z J A ) )
85 17 18 25 84 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Z ) = ( Z J A ) )
86 57 oveqd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Z J A ) = ( Z ( ( abs o. - ) |` ( RR X. RR ) ) A ) )
87 60 remetdval
 |-  ( ( Z e. RR /\ A e. RR ) -> ( Z ( ( abs o. - ) |` ( RR X. RR ) ) A ) = ( abs ` ( Z - A ) ) )
88 82 59 87 syl2anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( Z ( ( abs o. - ) |` ( RR X. RR ) ) A ) = ( abs ` ( Z - A ) ) )
89 85 86 88 3eqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A J Z ) = ( abs ` ( Z - A ) ) )
90 89 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A J Z ) = ( abs ` ( Z - A ) ) )
91 simprlr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A J Z ) < r )
92 90 91 eqbrtrrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( abs ` ( Z - A ) ) < r )
93 83 67 68 absdifltd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( abs ` ( Z - A ) ) < r <-> ( ( A - r ) < Z /\ Z < ( A + r ) ) ) )
94 92 93 mpbid
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) < Z /\ Z < ( A + r ) ) )
95 94 simpld
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( A - r ) < Z )
96 94 simprd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Z < ( A + r ) )
97 elioo2
 |-  ( ( ( A - r ) e. RR* /\ ( A + r ) e. RR* ) -> ( Z e. ( ( A - r ) (,) ( A + r ) ) <-> ( Z e. RR /\ ( A - r ) < Z /\ Z < ( A + r ) ) ) )
98 74 76 97 syl2anc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( Z e. ( ( A - r ) (,) ( A + r ) ) <-> ( Z e. RR /\ ( A - r ) < Z /\ Z < ( A + r ) ) ) )
99 83 95 96 98 mpbir3and
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Z e. ( ( A - r ) (,) ( A + r ) ) )
100 49 99 sselid
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> Z e. ( ( A - r ) [,] ( A + r ) ) )
101 100 fvresd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Z ) = ( F ` Z ) )
102 81 101 oveq12d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Y ) - ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Z ) ) = ( ( F ` Y ) - ( F ` Z ) ) )
103 102 fveq2d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( abs ` ( ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Y ) - ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Z ) ) ) = ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) )
104 17 ad3antrrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> J e. ( *Met ` S ) )
105 elicc2
 |-  ( ( ( A - r ) e. RR /\ ( A + r ) e. RR ) -> ( x e. ( ( A - r ) [,] ( A + r ) ) <-> ( x e. RR /\ ( A - r ) <_ x /\ x <_ ( A + r ) ) ) )
106 73 75 105 syl2anc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( x e. ( ( A - r ) [,] ( A + r ) ) <-> ( x e. RR /\ ( A - r ) <_ x /\ x <_ ( A + r ) ) ) )
107 106 biimpa
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x e. RR /\ ( A - r ) <_ x /\ x <_ ( A + r ) ) )
108 107 simp1d
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> x e. RR )
109 50 ad3antrrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> S = RR )
110 108 109 eleqtrrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> x e. S )
111 18 ad3antrrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> A e. S )
112 xmetcl
 |-  ( ( J e. ( *Met ` S ) /\ x e. S /\ A e. S ) -> ( x J A ) e. RR* )
113 104 110 111 112 syl3anc
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x J A ) e. RR* )
114 68 adantr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> r e. RR )
115 114 rexrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> r e. RR* )
116 21 ad3antrrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> R e. RR* )
117 57 ad3antrrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> J = ( ( abs o. - ) |` ( RR X. RR ) ) )
118 117 oveqd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x J A ) = ( x ( ( abs o. - ) |` ( RR X. RR ) ) A ) )
119 67 adantr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> A e. RR )
120 60 remetdval
 |-  ( ( x e. RR /\ A e. RR ) -> ( x ( ( abs o. - ) |` ( RR X. RR ) ) A ) = ( abs ` ( x - A ) ) )
121 108 119 120 syl2anc
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x ( ( abs o. - ) |` ( RR X. RR ) ) A ) = ( abs ` ( x - A ) ) )
122 118 121 eqtrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x J A ) = ( abs ` ( x - A ) ) )
123 107 simp2d
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( A - r ) <_ x )
124 107 simp3d
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> x <_ ( A + r ) )
125 108 119 114 absdifled
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( ( abs ` ( x - A ) ) <_ r <-> ( ( A - r ) <_ x /\ x <_ ( A + r ) ) ) )
126 123 124 125 mpbir2and
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( abs ` ( x - A ) ) <_ r )
127 122 126 eqbrtrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x J A ) <_ r )
128 simplrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> r < R )
129 113 115 116 127 128 xrlelttrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x J A ) < R )
130 elbl3
 |-  ( ( ( J e. ( *Met ` S ) /\ R e. RR* ) /\ ( A e. S /\ x e. S ) ) -> ( x e. ( A ( ball ` J ) R ) <-> ( x J A ) < R ) )
131 104 116 111 110 130 syl22anc
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> ( x e. ( A ( ball ` J ) R ) <-> ( x J A ) < R ) )
132 129 131 mpbird
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) [,] ( A + r ) ) ) -> x e. ( A ( ball ` J ) R ) )
133 132 ex
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( x e. ( ( A - r ) [,] ( A + r ) ) -> x e. ( A ( ball ` J ) R ) ) )
134 133 ssrdv
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) [,] ( A + r ) ) C_ ( A ( ball ` J ) R ) )
135 134 7 sseqtrrdi
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) [,] ( A + r ) ) C_ B )
136 135 resabs1d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( F |` B ) |` ( ( A - r ) [,] ( A + r ) ) ) = ( F |` ( ( A - r ) [,] ( A + r ) ) ) )
137 ax-resscn
 |-  RR C_ CC
138 137 a1i
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> RR C_ CC )
139 4 ad4antr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> F : X --> CC )
140 13 4 3 dvbss
 |-  ( ph -> dom ( S _D F ) C_ X )
141 8 140 sstrd
 |-  ( ph -> B C_ X )
142 141 ad4antr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> B C_ X )
143 139 142 fssresd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( F |` B ) : B --> CC )
144 blssm
 |-  ( ( J e. ( *Met ` S ) /\ A e. S /\ R e. RR* ) -> ( A ( ball ` J ) R ) C_ S )
145 17 18 21 144 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A ( ball ` J ) R ) C_ S )
146 7 145 eqsstrid
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> B C_ S )
147 146 50 sseqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> B C_ RR )
148 147 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> B C_ RR )
149 137 a1i
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> RR C_ CC )
150 4 ad2antrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> F : X --> CC )
151 3 ad2antrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> X C_ S )
152 151 50 sseqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> X C_ RR )
153 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
154 153 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
155 153 154 dvres
 |-  ( ( ( RR C_ CC /\ F : X --> CC ) /\ ( X C_ RR /\ B C_ RR ) ) -> ( RR _D ( F |` B ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` B ) ) )
156 149 150 152 147 155 syl22anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( RR _D ( F |` B ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` B ) ) )
157 retop
 |-  ( topGen ` ran (,) ) e. Top
158 57 fveq2d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ball ` J ) = ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) )
159 158 oveqd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A ( ball ` J ) R ) = ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) R ) )
160 7 159 eqtrid
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> B = ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) R ) )
161 57 17 eqeltrrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` S ) )
162 eqid
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
163 60 162 tgioo
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
164 163 blopn
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` S ) /\ A e. S /\ R e. RR* ) -> ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) R ) e. ( topGen ` ran (,) ) )
165 161 18 21 164 syl3anc
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( A ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) R ) e. ( topGen ` ran (,) ) )
166 160 165 eqeltrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> B e. ( topGen ` ran (,) ) )
167 isopn3i
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ B e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` B ) = B )
168 157 166 167 sylancr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` B ) = B )
169 168 reseq2d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` B ) ) = ( ( RR _D F ) |` B ) )
170 156 169 eqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( RR _D ( F |` B ) ) = ( ( RR _D F ) |` B ) )
171 170 dmeqd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> dom ( RR _D ( F |` B ) ) = dom ( ( RR _D F ) |` B ) )
172 dmres
 |-  dom ( ( RR _D F ) |` B ) = ( B i^i dom ( RR _D F ) )
173 8 ad2antrr
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> B C_ dom ( S _D F ) )
174 50 oveq1d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( S _D F ) = ( RR _D F ) )
175 174 dmeqd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> dom ( S _D F ) = dom ( RR _D F ) )
176 173 175 sseqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> B C_ dom ( RR _D F ) )
177 df-ss
 |-  ( B C_ dom ( RR _D F ) <-> ( B i^i dom ( RR _D F ) ) = B )
178 176 177 sylib
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( B i^i dom ( RR _D F ) ) = B )
179 172 178 eqtrid
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> dom ( ( RR _D F ) |` B ) = B )
180 171 179 eqtrd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> dom ( RR _D ( F |` B ) ) = B )
181 180 ad2antrr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> dom ( RR _D ( F |` B ) ) = B )
182 dvcn
 |-  ( ( ( RR C_ CC /\ ( F |` B ) : B --> CC /\ B C_ RR ) /\ dom ( RR _D ( F |` B ) ) = B ) -> ( F |` B ) e. ( B -cn-> CC ) )
183 138 143 148 181 182 syl31anc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( F |` B ) e. ( B -cn-> CC ) )
184 rescncf
 |-  ( ( ( A - r ) [,] ( A + r ) ) C_ B -> ( ( F |` B ) e. ( B -cn-> CC ) -> ( ( F |` B ) |` ( ( A - r ) [,] ( A + r ) ) ) e. ( ( ( A - r ) [,] ( A + r ) ) -cn-> CC ) ) )
185 135 183 184 sylc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( F |` B ) |` ( ( A - r ) [,] ( A + r ) ) ) e. ( ( ( A - r ) [,] ( A + r ) ) -cn-> CC ) )
186 136 185 eqeltrrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( F |` ( ( A - r ) [,] ( A + r ) ) ) e. ( ( ( A - r ) [,] ( A + r ) ) -cn-> CC ) )
187 135 148 sstrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) [,] ( A + r ) ) C_ RR )
188 153 154 dvres
 |-  ( ( ( RR C_ CC /\ ( F |` B ) : B --> CC ) /\ ( B C_ RR /\ ( ( A - r ) [,] ( A + r ) ) C_ RR ) ) -> ( RR _D ( ( F |` B ) |` ( ( A - r ) [,] ( A + r ) ) ) ) = ( ( RR _D ( F |` B ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A - r ) [,] ( A + r ) ) ) ) )
189 138 143 148 187 188 syl22anc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( RR _D ( ( F |` B ) |` ( ( A - r ) [,] ( A + r ) ) ) ) = ( ( RR _D ( F |` B ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A - r ) [,] ( A + r ) ) ) ) )
190 136 oveq2d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( RR _D ( ( F |` B ) |` ( ( A - r ) [,] ( A + r ) ) ) ) = ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) )
191 iccntr
 |-  ( ( ( A - r ) e. RR /\ ( A + r ) e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A - r ) [,] ( A + r ) ) ) = ( ( A - r ) (,) ( A + r ) ) )
192 73 75 191 syl2anc
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A - r ) [,] ( A + r ) ) ) = ( ( A - r ) (,) ( A + r ) ) )
193 192 reseq2d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( RR _D ( F |` B ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A - r ) [,] ( A + r ) ) ) ) = ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) )
194 189 190 193 3eqtr3d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) = ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) )
195 194 dmeqd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> dom ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) = dom ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) )
196 dmres
 |-  dom ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) = ( ( ( A - r ) (,) ( A + r ) ) i^i dom ( RR _D ( F |` B ) ) )
197 49 135 sstrid
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) (,) ( A + r ) ) C_ B )
198 197 181 sseqtrrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( A - r ) (,) ( A + r ) ) C_ dom ( RR _D ( F |` B ) ) )
199 df-ss
 |-  ( ( ( A - r ) (,) ( A + r ) ) C_ dom ( RR _D ( F |` B ) ) <-> ( ( ( A - r ) (,) ( A + r ) ) i^i dom ( RR _D ( F |` B ) ) ) = ( ( A - r ) (,) ( A + r ) ) )
200 198 199 sylib
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( ( A - r ) (,) ( A + r ) ) i^i dom ( RR _D ( F |` B ) ) ) = ( ( A - r ) (,) ( A + r ) ) )
201 196 200 eqtrid
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> dom ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) = ( ( A - r ) (,) ( A + r ) ) )
202 195 201 eqtrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> dom ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) = ( ( A - r ) (,) ( A + r ) ) )
203 9 ad4antr
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> M e. RR )
204 194 fveq1d
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) ` x ) = ( ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) ` x ) )
205 fvres
 |-  ( x e. ( ( A - r ) (,) ( A + r ) ) -> ( ( ( RR _D ( F |` B ) ) |` ( ( A - r ) (,) ( A + r ) ) ) ` x ) = ( ( RR _D ( F |` B ) ) ` x ) )
206 204 205 sylan9eq
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) ` x ) = ( ( RR _D ( F |` B ) ) ` x ) )
207 174 reseq1d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ( S _D F ) |` B ) = ( ( RR _D F ) |` B ) )
208 170 207 eqtr4d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( RR _D ( F |` B ) ) = ( ( S _D F ) |` B ) )
209 208 fveq1d
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( ( RR _D ( F |` B ) ) ` x ) = ( ( ( S _D F ) |` B ) ` x ) )
210 209 ad3antrrr
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( ( RR _D ( F |` B ) ) ` x ) = ( ( ( S _D F ) |` B ) ` x ) )
211 197 sselda
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> x e. B )
212 211 fvresd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( ( ( S _D F ) |` B ) ` x ) = ( ( S _D F ) ` x ) )
213 206 210 212 3eqtrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) ` x ) = ( ( S _D F ) ` x ) )
214 213 fveq2d
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) ` x ) ) = ( abs ` ( ( S _D F ) ` x ) ) )
215 simp-4l
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ph )
216 215 211 10 syl2an2r
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( abs ` ( ( S _D F ) ` x ) ) <_ M )
217 214 216 eqbrtrd
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ x e. ( ( A - r ) (,) ( A + r ) ) ) -> ( abs ` ( ( RR _D ( F |` ( ( A - r ) [,] ( A + r ) ) ) ) ` x ) ) <_ M )
218 73 75 186 202 203 217 dvlip
 |-  ( ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) /\ ( Y e. ( ( A - r ) [,] ( A + r ) ) /\ Z e. ( ( A - r ) [,] ( A + r ) ) ) ) -> ( abs ` ( ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Y ) - ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
219 218 ex
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( ( Y e. ( ( A - r ) [,] ( A + r ) ) /\ Z e. ( ( A - r ) [,] ( A + r ) ) ) -> ( abs ` ( ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Y ) - ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) )
220 80 100 219 mp2and
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( abs ` ( ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Y ) - ( ( F |` ( ( A - r ) [,] ( A + r ) ) ) ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
221 103 220 eqbrtrrd
 |-  ( ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) /\ ( ( ( A J Y ) < r /\ ( A J Z ) < r ) /\ r < R ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
222 221 exp32
 |-  ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) -> ( ( ( A J Y ) < r /\ ( A J Z ) < r ) -> ( r < R -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) ) )
223 48 222 sylbid
 |-  ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) -> ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r -> ( r < R -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) ) )
224 223 impd
 |-  ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. RR ) -> ( ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r /\ r < R ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) )
225 45 224 sylan2
 |-  ( ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) /\ r e. QQ ) -> ( ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r /\ r < R ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) )
226 225 rexlimdva
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( E. r e. QQ ( if ( ( A J Y ) <_ ( A J Z ) , ( A J Z ) , ( A J Y ) ) < r /\ r < R ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) )
227 44 226 mpd
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = RR ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
228 simpr
 |-  ( ( ph /\ S = CC ) -> S = CC )
229 228 sqxpeqd
 |-  ( ( ph /\ S = CC ) -> ( S X. S ) = ( CC X. CC ) )
230 229 reseq2d
 |-  ( ( ph /\ S = CC ) -> ( ( abs o. - ) |` ( S X. S ) ) = ( ( abs o. - ) |` ( CC X. CC ) ) )
231 absf
 |-  abs : CC --> RR
232 subf
 |-  - : ( CC X. CC ) --> CC
233 fco
 |-  ( ( abs : CC --> RR /\ - : ( CC X. CC ) --> CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )
234 231 232 233 mp2an
 |-  ( abs o. - ) : ( CC X. CC ) --> RR
235 ffn
 |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )
236 fnresdm
 |-  ( ( abs o. - ) Fn ( CC X. CC ) -> ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - ) )
237 234 235 236 mp2b
 |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - )
238 230 237 eqtrdi
 |-  ( ( ph /\ S = CC ) -> ( ( abs o. - ) |` ( S X. S ) ) = ( abs o. - ) )
239 2 238 eqtrid
 |-  ( ( ph /\ S = CC ) -> J = ( abs o. - ) )
240 239 fveq2d
 |-  ( ( ph /\ S = CC ) -> ( ball ` J ) = ( ball ` ( abs o. - ) ) )
241 240 oveqd
 |-  ( ( ph /\ S = CC ) -> ( A ( ball ` J ) R ) = ( A ( ball ` ( abs o. - ) ) R ) )
242 7 241 eqtrid
 |-  ( ( ph /\ S = CC ) -> B = ( A ( ball ` ( abs o. - ) ) R ) )
243 242 eleq2d
 |-  ( ( ph /\ S = CC ) -> ( Y e. B <-> Y e. ( A ( ball ` ( abs o. - ) ) R ) ) )
244 242 eleq2d
 |-  ( ( ph /\ S = CC ) -> ( Z e. B <-> Z e. ( A ( ball ` ( abs o. - ) ) R ) ) )
245 243 244 anbi12d
 |-  ( ( ph /\ S = CC ) -> ( ( Y e. B /\ Z e. B ) <-> ( Y e. ( A ( ball ` ( abs o. - ) ) R ) /\ Z e. ( A ( ball ` ( abs o. - ) ) R ) ) ) )
246 245 biimpa
 |-  ( ( ( ph /\ S = CC ) /\ ( Y e. B /\ Z e. B ) ) -> ( Y e. ( A ( ball ` ( abs o. - ) ) R ) /\ Z e. ( A ( ball ` ( abs o. - ) ) R ) ) )
247 3 adantr
 |-  ( ( ph /\ S = CC ) -> X C_ S )
248 247 228 sseqtrd
 |-  ( ( ph /\ S = CC ) -> X C_ CC )
249 4 adantr
 |-  ( ( ph /\ S = CC ) -> F : X --> CC )
250 5 adantr
 |-  ( ( ph /\ S = CC ) -> A e. S )
251 250 228 eleqtrd
 |-  ( ( ph /\ S = CC ) -> A e. CC )
252 6 adantr
 |-  ( ( ph /\ S = CC ) -> R e. RR* )
253 eqid
 |-  ( A ( ball ` ( abs o. - ) ) R ) = ( A ( ball ` ( abs o. - ) ) R )
254 8 adantr
 |-  ( ( ph /\ S = CC ) -> B C_ dom ( S _D F ) )
255 228 oveq1d
 |-  ( ( ph /\ S = CC ) -> ( S _D F ) = ( CC _D F ) )
256 255 dmeqd
 |-  ( ( ph /\ S = CC ) -> dom ( S _D F ) = dom ( CC _D F ) )
257 254 242 256 3sstr3d
 |-  ( ( ph /\ S = CC ) -> ( A ( ball ` ( abs o. - ) ) R ) C_ dom ( CC _D F ) )
258 9 adantr
 |-  ( ( ph /\ S = CC ) -> M e. RR )
259 10 ex
 |-  ( ph -> ( x e. B -> ( abs ` ( ( S _D F ) ` x ) ) <_ M ) )
260 259 adantr
 |-  ( ( ph /\ S = CC ) -> ( x e. B -> ( abs ` ( ( S _D F ) ` x ) ) <_ M ) )
261 242 eleq2d
 |-  ( ( ph /\ S = CC ) -> ( x e. B <-> x e. ( A ( ball ` ( abs o. - ) ) R ) ) )
262 255 fveq1d
 |-  ( ( ph /\ S = CC ) -> ( ( S _D F ) ` x ) = ( ( CC _D F ) ` x ) )
263 262 fveq2d
 |-  ( ( ph /\ S = CC ) -> ( abs ` ( ( S _D F ) ` x ) ) = ( abs ` ( ( CC _D F ) ` x ) ) )
264 263 breq1d
 |-  ( ( ph /\ S = CC ) -> ( ( abs ` ( ( S _D F ) ` x ) ) <_ M <-> ( abs ` ( ( CC _D F ) ` x ) ) <_ M ) )
265 260 261 264 3imtr3d
 |-  ( ( ph /\ S = CC ) -> ( x e. ( A ( ball ` ( abs o. - ) ) R ) -> ( abs ` ( ( CC _D F ) ` x ) ) <_ M ) )
266 265 imp
 |-  ( ( ( ph /\ S = CC ) /\ x e. ( A ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( ( CC _D F ) ` x ) ) <_ M )
267 248 249 251 252 253 257 258 266 dvlipcn
 |-  ( ( ( ph /\ S = CC ) /\ ( Y e. ( A ( ball ` ( abs o. - ) ) R ) /\ Z e. ( A ( ball ` ( abs o. - ) ) R ) ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
268 246 267 syldan
 |-  ( ( ( ph /\ S = CC ) /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
269 268 an32s
 |-  ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ S = CC ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
270 elpri
 |-  ( S e. { RR , CC } -> ( S = RR \/ S = CC ) )
271 1 270 syl
 |-  ( ph -> ( S = RR \/ S = CC ) )
272 271 adantr
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( S = RR \/ S = CC ) )
273 227 269 272 mpjaodan
 |-  ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )