Metamath Proof Explorer

Theorem minveclem4

Description: Lemma for minvec . The convergent point of the Cauchy sequence F attains the minimum distance, and so is closer to A than any other point in Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses minvec.x 
|- X = ( Base ` U )
minvec.m 
|- .- = ( -g ` U )
minvec.n 
|- N = ( norm ` U )
minvec.u 
|- ( ph -> U e. CPreHil )
minvec.y 
|- ( ph -> Y e. ( LSubSp ` U ) )
minvec.w 
|- ( ph -> ( U |`s Y ) e. CMetSp )
minvec.a 
|- ( ph -> A e. X )
minvec.j 
|- J = ( TopOpen ` U )
minvec.r 
|- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
minvec.s 
|- S = inf ( R , RR , < )
minvec.d 
|- D = ( ( dist ` U ) |` ( X X. X ) )
minvec.f 
|- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
minvec.p 
|- P = U. ( J fLim ( X filGen F ) )
minvec.t 
|- T = ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) )
Assertion minveclem4 
|- ( ph -> E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )

Proof

Step Hyp Ref Expression
1 minvec.x 
 |-  X = ( Base ` U )
2 minvec.m 
 |-  .- = ( -g ` U )
3 minvec.n 
 |-  N = ( norm ` U )
4 minvec.u 
 |-  ( ph -> U e. CPreHil )
5 minvec.y 
 |-  ( ph -> Y e. ( LSubSp ` U ) )
6 minvec.w 
 |-  ( ph -> ( U |`s Y ) e. CMetSp )
7 minvec.a 
 |-  ( ph -> A e. X )
8 minvec.j 
 |-  J = ( TopOpen ` U )
9 minvec.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
10 minvec.s 
 |-  S = inf ( R , RR , < )
11 minvec.d 
 |-  D = ( ( dist ` U ) |` ( X X. X ) )
12 minvec.f 
 |-  F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
13 minvec.p 
 |-  P = U. ( J fLim ( X filGen F ) )
14 minvec.t 
 |-  T = ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 minveclem4a 
 |-  ( ph -> P e. ( ( J fLim ( X filGen F ) ) i^i Y ) )
16 15 elin2d 
 |-  ( ph -> P e. Y )
17 11 oveqi 
 |-  ( A D P ) = ( A ( ( dist ` U ) |` ( X X. X ) ) P )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 minveclem4b 
 |-  ( ph -> P e. X )
19 7 18 ovresd 
 |-  ( ph -> ( A ( ( dist ` U ) |` ( X X. X ) ) P ) = ( A ( dist ` U ) P ) )
20 17 19 syl5eq 
 |-  ( ph -> ( A D P ) = ( A ( dist ` U ) P ) )
21 cphngp 
 |-  ( U e. CPreHil -> U e. NrmGrp )
22 4 21 syl 
 |-  ( ph -> U e. NrmGrp )
23 eqid 
 |-  ( dist ` U ) = ( dist ` U )
24 3 1 2 23 ngpds 
 |-  ( ( U e. NrmGrp /\ A e. X /\ P e. X ) -> ( A ( dist ` U ) P ) = ( N ` ( A .- P ) ) )
25 22 7 18 24 syl3anc 
 |-  ( ph -> ( A ( dist ` U ) P ) = ( N ` ( A .- P ) ) )
26 20 25 eqtrd 
 |-  ( ph -> ( A D P ) = ( N ` ( A .- P ) ) )
27 26 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( A D P ) = ( N ` ( A .- P ) ) )
28 ngpms 
 |-  ( U e. NrmGrp -> U e. MetSp )
29 1 11 msmet 
 |-  ( U e. MetSp -> D e. ( Met ` X ) )
30 22 28 29 3syl 
 |-  ( ph -> D e. ( Met ` X ) )
31 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ P e. X ) -> ( A D P ) e. RR )
32 30 7 18 31 syl3anc 
 |-  ( ph -> ( A D P ) e. RR )
33 32 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( A D P ) e. RR )
34 1 2 3 4 5 6 7 8 9 10 minveclem4c 
 |-  ( ph -> S e. RR )
35 34 adantr 
 |-  ( ( ph /\ y e. Y ) -> S e. RR )
36 22 adantr 
 |-  ( ( ph /\ y e. Y ) -> U e. NrmGrp )
37 cphlmod 
 |-  ( U e. CPreHil -> U e. LMod )
38 4 37 syl 
 |-  ( ph -> U e. LMod )
39 38 adantr 
 |-  ( ( ph /\ y e. Y ) -> U e. LMod )
40 7 adantr 
 |-  ( ( ph /\ y e. Y ) -> A e. X )
41 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
42 1 41 lssss 
 |-  ( Y e. ( LSubSp ` U ) -> Y C_ X )
43 5 42 syl 
 |-  ( ph -> Y C_ X )
44 43 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. X )
45 1 2 lmodvsubcl 
 |-  ( ( U e. LMod /\ A e. X /\ y e. X ) -> ( A .- y ) e. X )
46 39 40 44 45 syl3anc 
 |-  ( ( ph /\ y e. Y ) -> ( A .- y ) e. X )
47 1 3 nmcl 
 |-  ( ( U e. NrmGrp /\ ( A .- y ) e. X ) -> ( N ` ( A .- y ) ) e. RR )
48 36 46 47 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A .- y ) ) e. RR )
49 34 32 ltnled 
 |-  ( ph -> ( S < ( A D P ) <-> -. ( A D P ) <_ S ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 minveclem3b 
 |-  ( ph -> F e. ( fBas ` Y ) )
51 fbsspw 
 |-  ( F e. ( fBas ` Y ) -> F C_ ~P Y )
52 50 51 syl 
 |-  ( ph -> F C_ ~P Y )
53 43 sspwd 
 |-  ( ph -> ~P Y C_ ~P X )
54 52 53 sstrd 
 |-  ( ph -> F C_ ~P X )
55 1 fvexi 
 |-  X e. _V
56 55 a1i 
 |-  ( ph -> X e. _V )
57 fbasweak 
 |-  ( ( F e. ( fBas ` Y ) /\ F C_ ~P X /\ X e. _V ) -> F e. ( fBas ` X ) )
58 50 54 56 57 syl3anc 
 |-  ( ph -> F e. ( fBas ` X ) )
59 58 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> F e. ( fBas ` X ) )
60 fgcl 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) e. ( Fil ` X ) )
61 59 60 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( X filGen F ) e. ( Fil ` X ) )
62 ssfg 
 |-  ( F e. ( fBas ` X ) -> F C_ ( X filGen F ) )
63 59 62 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> F C_ ( X filGen F ) )
64 32 34 readdcld 
 |-  ( ph -> ( ( A D P ) + S ) e. RR )
65 64 rehalfcld 
 |-  ( ph -> ( ( ( A D P ) + S ) / 2 ) e. RR )
66 65 resqcld 
 |-  ( ph -> ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) e. RR )
67 34 resqcld 
 |-  ( ph -> ( S ^ 2 ) e. RR )
68 66 67 resubcld 
 |-  ( ph -> ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR )
69 68 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR )
70 34 32 34 ltadd1d 
 |-  ( ph -> ( S < ( A D P ) <-> ( S + S ) < ( ( A D P ) + S ) ) )
71 34 recnd 
 |-  ( ph -> S e. CC )
72 71 2timesd 
 |-  ( ph -> ( 2 x. S ) = ( S + S ) )
73 72 breq1d 
 |-  ( ph -> ( ( 2 x. S ) < ( ( A D P ) + S ) <-> ( S + S ) < ( ( A D P ) + S ) ) )
74 2re 
 |-  2 e. RR
75 2pos 
 |-  0 < 2
76 74 75 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
77 76 a1i 
 |-  ( ph -> ( 2 e. RR /\ 0 < 2 ) )
78 ltmuldiv2 
 |-  ( ( S e. RR /\ ( ( A D P ) + S ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. S ) < ( ( A D P ) + S ) <-> S < ( ( ( A D P ) + S ) / 2 ) ) )
79 34 64 77 78 syl3anc 
 |-  ( ph -> ( ( 2 x. S ) < ( ( A D P ) + S ) <-> S < ( ( ( A D P ) + S ) / 2 ) ) )
80 70 73 79 3bitr2d 
 |-  ( ph -> ( S < ( A D P ) <-> S < ( ( ( A D P ) + S ) / 2 ) ) )
81 1 2 3 4 5 6 7 8 9 minveclem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
82 81 simp3d 
 |-  ( ph -> A. w e. R 0 <_ w )
83 81 simp1d 
 |-  ( ph -> R C_ RR )
84 81 simp2d 
 |-  ( ph -> R =/= (/) )
85 0re 
 |-  0 e. RR
86 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
87 86 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
88 87 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
89 85 82 88 sylancr 
 |-  ( ph -> E. x e. RR A. w e. R x <_ w )
90 85 a1i 
 |-  ( ph -> 0 e. RR )
91 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ 0 e. RR ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
92 83 84 89 90 91 syl31anc 
 |-  ( ph -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
93 82 92 mpbird 
 |-  ( ph -> 0 <_ inf ( R , RR , < ) )
94 93 10 breqtrrdi 
 |-  ( ph -> 0 <_ S )
95 metge0 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ P e. X ) -> 0 <_ ( A D P ) )
96 30 7 18 95 syl3anc 
 |-  ( ph -> 0 <_ ( A D P ) )
97 32 34 96 94 addge0d 
 |-  ( ph -> 0 <_ ( ( A D P ) + S ) )
98 divge0 
 |-  ( ( ( ( ( A D P ) + S ) e. RR /\ 0 <_ ( ( A D P ) + S ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( ( A D P ) + S ) / 2 ) )
99 64 97 77 98 syl21anc 
 |-  ( ph -> 0 <_ ( ( ( A D P ) + S ) / 2 ) )
100 34 65 94 99 lt2sqd 
 |-  ( ph -> ( S < ( ( ( A D P ) + S ) / 2 ) <-> ( S ^ 2 ) < ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) ) )
101 67 66 posdifd 
 |-  ( ph -> ( ( S ^ 2 ) < ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) <-> 0 < ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
102 80 100 101 3bitrd 
 |-  ( ph -> ( S < ( A D P ) <-> 0 < ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
103 102 biimpa 
 |-  ( ( ph /\ S < ( A D P ) ) -> 0 < ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
104 69 103 elrpd 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR+ )
105 14 104 eqeltrid 
 |-  ( ( ph /\ S < ( A D P ) ) -> T e. RR+ )
106 5 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> Y e. ( LSubSp ` U ) )
107 rabexg 
 |-  ( Y e. ( LSubSp ` U ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. _V )
108 106 107 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. _V )
109 eqid 
 |-  ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) = ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )
110 oveq2 
 |-  ( r = T -> ( ( S ^ 2 ) + r ) = ( ( S ^ 2 ) + T ) )
111 110 breq2d 
 |-  ( r = T -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) <-> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) ) )
112 111 rabbidv 
 |-  ( r = T -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } = { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } )
113 109 112 elrnmpt1s 
 |-  ( ( T e. RR+ /\ { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. _V ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
114 105 108 113 syl2anc 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } ) )
115 114 12 eleqtrrdi 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. F )
116 63 115 sseldd 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. ( X filGen F ) )
117 ssrab2 
 |-  { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } C_ X
118 117 a1i 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } C_ X )
119 14 oveq2i 
 |-  ( ( S ^ 2 ) + T ) = ( ( S ^ 2 ) + ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
120 67 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( S ^ 2 ) e. RR )
121 120 recnd 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( S ^ 2 ) e. CC )
122 65 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( ( A D P ) + S ) / 2 ) e. RR )
123 122 resqcld 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) e. RR )
124 123 recnd 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) e. CC )
125 121 124 pncan3d 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( S ^ 2 ) + ( ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) = ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) )
126 119 125 syl5eq 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( S ^ 2 ) + T ) = ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) )
127 126 breq2d 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) <-> ( ( A D y ) ^ 2 ) <_ ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) ) )
128 30 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> D e. ( Met ` X ) )
129 7 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> A e. X )
130 44 adantlr 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> y e. X )
131 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ y e. X ) -> ( A D y ) e. RR )
132 128 129 130 131 syl3anc 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( A D y ) e. RR )
133 metge0 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ y e. X ) -> 0 <_ ( A D y ) )
134 128 129 130 133 syl3anc 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> 0 <_ ( A D y ) )
135 99 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> 0 <_ ( ( ( A D P ) + S ) / 2 ) )
136 132 122 134 135 le2sqd 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) <-> ( ( A D y ) ^ 2 ) <_ ( ( ( ( A D P ) + S ) / 2 ) ^ 2 ) ) )
137 127 136 bitr4d 
 |-  ( ( ( ph /\ S < ( A D P ) ) /\ y e. Y ) -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) <-> ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
138 137 rabbidva 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } = { y e. Y | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
139 43 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> Y C_ X )
140 rabss2 
 |-  ( Y C_ X -> { y e. Y | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } C_ { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
141 139 140 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } C_ { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
142 138 141 eqsstrd 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } C_ { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
143 filss 
 |-  ( ( ( X filGen F ) e. ( Fil ` X ) /\ ( { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } e. ( X filGen F ) /\ { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } C_ X /\ { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + T ) } C_ { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } ) ) -> { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( X filGen F ) )
144 61 116 118 142 143 syl13anc 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( X filGen F ) )
145 flimclsi 
 |-  ( { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( X filGen F ) -> ( J fLim ( X filGen F ) ) C_ ( ( cls ` J ) ` { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } ) )
146 144 145 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( J fLim ( X filGen F ) ) C_ ( ( cls ` J ) ` { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } ) )
147 15 elin1d 
 |-  ( ph -> P e. ( J fLim ( X filGen F ) ) )
148 147 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> P e. ( J fLim ( X filGen F ) ) )
149 146 148 sseldd 
 |-  ( ( ph /\ S < ( A D P ) ) -> P e. ( ( cls ` J ) ` { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } ) )
150 ngpxms 
 |-  ( U e. NrmGrp -> U e. *MetSp )
151 1 11 xmsxmet 
 |-  ( U e. *MetSp -> D e. ( *Met ` X ) )
152 22 150 151 3syl 
 |-  ( ph -> D e. ( *Met ` X ) )
153 152 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> D e. ( *Met ` X ) )
154 7 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> A e. X )
155 65 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( ( ( A D P ) + S ) / 2 ) e. RR )
156 155 rexrd 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( ( ( A D P ) + S ) / 2 ) e. RR* )
157 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
158 eqid 
 |-  { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } = { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) }
159 157 158 blcld 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ ( ( ( A D P ) + S ) / 2 ) e. RR* ) -> { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( Clsd ` ( MetOpen ` D ) ) )
160 153 154 156 159 syl3anc 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( Clsd ` ( MetOpen ` D ) ) )
161 8 1 11 xmstopn 
 |-  ( U e. *MetSp -> J = ( MetOpen ` D ) )
162 22 150 161 3syl 
 |-  ( ph -> J = ( MetOpen ` D ) )
163 162 adantr 
 |-  ( ( ph /\ S < ( A D P ) ) -> J = ( MetOpen ` D ) )
164 163 fveq2d 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( Clsd ` J ) = ( Clsd ` ( MetOpen ` D ) ) )
165 160 164 eleqtrrd 
 |-  ( ( ph /\ S < ( A D P ) ) -> { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( Clsd ` J ) )
166 cldcls 
 |-  ( { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } e. ( Clsd ` J ) -> ( ( cls ` J ) ` { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } ) = { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
167 165 166 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( ( cls ` J ) ` { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } ) = { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
168 149 167 eleqtrd 
 |-  ( ( ph /\ S < ( A D P ) ) -> P e. { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } )
169 oveq2 
 |-  ( y = P -> ( A D y ) = ( A D P ) )
170 169 breq1d 
 |-  ( y = P -> ( ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) <-> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
171 170 elrab 
 |-  ( P e. { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } <-> ( P e. X /\ ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
172 171 simprbi 
 |-  ( P e. { y e. X | ( A D y ) <_ ( ( ( A D P ) + S ) / 2 ) } -> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) )
173 168 172 syl 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) )
174 32 34 32 leadd2d 
 |-  ( ph -> ( ( A D P ) <_ S <-> ( ( A D P ) + ( A D P ) ) <_ ( ( A D P ) + S ) ) )
175 32 recnd 
 |-  ( ph -> ( A D P ) e. CC )
176 175 2timesd 
 |-  ( ph -> ( 2 x. ( A D P ) ) = ( ( A D P ) + ( A D P ) ) )
177 176 breq1d 
 |-  ( ph -> ( ( 2 x. ( A D P ) ) <_ ( ( A D P ) + S ) <-> ( ( A D P ) + ( A D P ) ) <_ ( ( A D P ) + S ) ) )
178 lemuldiv2 
 |-  ( ( ( A D P ) e. RR /\ ( ( A D P ) + S ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. ( A D P ) ) <_ ( ( A D P ) + S ) <-> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
179 76 178 mp3an3 
 |-  ( ( ( A D P ) e. RR /\ ( ( A D P ) + S ) e. RR ) -> ( ( 2 x. ( A D P ) ) <_ ( ( A D P ) + S ) <-> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
180 32 64 179 syl2anc 
 |-  ( ph -> ( ( 2 x. ( A D P ) ) <_ ( ( A D P ) + S ) <-> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
181 174 177 180 3bitr2d 
 |-  ( ph -> ( ( A D P ) <_ S <-> ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) )
182 181 biimpar 
 |-  ( ( ph /\ ( A D P ) <_ ( ( ( A D P ) + S ) / 2 ) ) -> ( A D P ) <_ S )
183 173 182 syldan 
 |-  ( ( ph /\ S < ( A D P ) ) -> ( A D P ) <_ S )
184 183 ex 
 |-  ( ph -> ( S < ( A D P ) -> ( A D P ) <_ S ) )
185 49 184 sylbird 
 |-  ( ph -> ( -. ( A D P ) <_ S -> ( A D P ) <_ S ) )
186 185 pm2.18d 
 |-  ( ph -> ( A D P ) <_ S )
187 186 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( A D P ) <_ S )
188 83 adantr 
 |-  ( ( ph /\ y e. Y ) -> R C_ RR )
189 89 adantr 
 |-  ( ( ph /\ y e. Y ) -> E. x e. RR A. w e. R x <_ w )
190 simpr 
 |-  ( ( ph /\ y e. Y ) -> y e. Y )
191 fvex 
 |-  ( N ` ( A .- y ) ) e. _V
192 eqid 
 |-  ( y e. Y |-> ( N ` ( A .- y ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) )
193 192 elrnmpt1 
 |-  ( ( y e. Y /\ ( N ` ( A .- y ) ) e. _V ) -> ( N ` ( A .- y ) ) e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) )
194 190 191 193 sylancl 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A .- y ) ) e. ran ( y e. Y |-> ( N ` ( A .- y ) ) ) )
195 194 9 eleqtrrdi 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A .- y ) ) e. R )
196 infrelb 
 |-  ( ( R C_ RR /\ E. x e. RR A. w e. R x <_ w /\ ( N ` ( A .- y ) ) e. R ) -> inf ( R , RR , < ) <_ ( N ` ( A .- y ) ) )
197 188 189 195 196 syl3anc 
 |-  ( ( ph /\ y e. Y ) -> inf ( R , RR , < ) <_ ( N ` ( A .- y ) ) )
198 10 197 eqbrtrid 
 |-  ( ( ph /\ y e. Y ) -> S <_ ( N ` ( A .- y ) ) )
199 33 35 48 187 198 letrd 
 |-  ( ( ph /\ y e. Y ) -> ( A D P ) <_ ( N ` ( A .- y ) ) )
200 27 199 eqbrtrrd 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A .- P ) ) <_ ( N ` ( A .- y ) ) )
201 200 ralrimiva 
 |-  ( ph -> A. y e. Y ( N ` ( A .- P ) ) <_ ( N ` ( A .- y ) ) )
202 oveq2 
 |-  ( x = P -> ( A .- x ) = ( A .- P ) )
203 202 fveq2d 
 |-  ( x = P -> ( N ` ( A .- x ) ) = ( N ` ( A .- P ) ) )
204 203 breq1d 
 |-  ( x = P -> ( ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) <-> ( N ` ( A .- P ) ) <_ ( N ` ( A .- y ) ) ) )
205 204 ralbidv 
 |-  ( x = P -> ( A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) <-> A. y e. Y ( N ` ( A .- P ) ) <_ ( N ` ( A .- y ) ) ) )
206 205 rspcev 
 |-  ( ( P e. Y /\ A. y e. Y ( N ` ( A .- P ) ) <_ ( N ` ( A .- y ) ) ) -> E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )
207 16 201 206 syl2anc 
 |-  ( ph -> E. x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )