This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem minvecolem4c

Description: Lemma for minveco . The infimum of the distances to A is a real number. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses minveco.x 
|- X = ( BaseSet ` U )
minveco.m 
|- M = ( -v ` U )
minveco.n 
|- N = ( normCV ` U )
minveco.y 
|- Y = ( BaseSet ` W )
minveco.u 
|- ( ph -> U e. CPreHilOLD )
minveco.w 
|- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
minveco.a 
|- ( ph -> A e. X )
minveco.d 
|- D = ( IndMet ` U )
minveco.j 
|- J = ( MetOpen ` D )
minveco.r 
|- R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
minveco.s 
|- S = inf ( R , RR , < )
minveco.f 
|- ( ph -> F : NN --> Y )
minveco.1 
|- ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
Assertion minvecolem4c 
|- ( ph -> S e. RR )

Proof

Step Hyp Ref Expression
1 minveco.x 
 |-  X = ( BaseSet ` U )
2 minveco.m 
 |-  M = ( -v ` U )
3 minveco.n 
 |-  N = ( normCV ` U )
4 minveco.y 
 |-  Y = ( BaseSet ` W )
5 minveco.u 
 |-  ( ph -> U e. CPreHilOLD )
6 minveco.w 
 |-  ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
7 minveco.a 
 |-  ( ph -> A e. X )
8 minveco.d 
 |-  D = ( IndMet ` U )
9 minveco.j 
 |-  J = ( MetOpen ` D )
10 minveco.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
11 minveco.s 
 |-  S = inf ( R , RR , < )
12 minveco.f 
 |-  ( ph -> F : NN --> Y )
13 minveco.1 
 |-  ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
14 1 2 3 4 5 6 7 8 9 10 minvecolem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
15 14 simp1d 
 |-  ( ph -> R C_ RR )
16 14 simp2d 
 |-  ( ph -> R =/= (/) )
17 0re 
 |-  0 e. RR
18 14 simp3d 
 |-  ( ph -> A. w e. R 0 <_ w )
19 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
20 19 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
21 20 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
22 17 18 21 sylancr 
 |-  ( ph -> E. x e. RR A. w e. R x <_ w )
23 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR )
24 15 16 22 23 syl3anc 
 |-  ( ph -> inf ( R , RR , < ) e. RR )
25 11 24 eqeltrid 
 |-  ( ph -> S e. RR )