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 syl5eq 
 |-  ( ( ( 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 syl5eq 
 |-  ( ( ( 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 syl5eq 
 |-  ( ( ( 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 syl5eq 
 |-  ( ( ( ( ( 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 syl5eq 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 ) ) ) )