Metamath Proof Explorer


Theorem minveclem4c

Description: Lemma for minvec . The infimum of the distances to A is a real number. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses minvec.x X=BaseU
minvec.m -˙=-U
minvec.n N=normU
minvec.u φUCPreHil
minvec.y φYLSubSpU
minvec.w φU𝑠YCMetSp
minvec.a φAX
minvec.j J=TopOpenU
minvec.r R=ranyYNA-˙y
minvec.s S=supR<
Assertion minveclem4c φS

Proof

Step Hyp Ref Expression
1 minvec.x X=BaseU
2 minvec.m -˙=-U
3 minvec.n N=normU
4 minvec.u φUCPreHil
5 minvec.y φYLSubSpU
6 minvec.w φU𝑠YCMetSp
7 minvec.a φAX
8 minvec.j J=TopOpenU
9 minvec.r R=ranyYNA-˙y
10 minvec.s S=supR<
11 1 2 3 4 5 6 7 8 9 minveclem1 φRRwR0w
12 11 simp1d φR
13 11 simp2d φR
14 0re 0
15 11 simp3d φwR0w
16 breq1 y=0yw0w
17 16 ralbidv y=0wRywwR0w
18 17 rspcev 0wR0wywRyw
19 14 15 18 sylancr φywRyw
20 infrecl RRywRywsupR<
21 12 13 19 20 syl3anc φsupR<
22 10 21 eqeltrid φS