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 )

Metamath Proof Explorer

Theorem minvecolem4c

Proof