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 = ( 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 , < )
Assertion	minveclem4c	|- ( ph -> S e. RR )

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	1 2 3 4 5 6 7 8 9	minveclem1	|- ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
12	11	simp1d	|- ( ph -> R C_ RR )
13	11	simp2d	|- ( ph -> R =/= (/) )
14		0re	|- 0 e. RR
15	11	simp3d	|- ( ph -> A. w e. R 0 <_ w )
16		breq1	|- ( y = 0 -> ( y <_ w <-> 0 <_ w ) )
17	16	ralbidv	|- ( y = 0 -> ( A. w e. R y <_ w <-> A. w e. R 0 <_ w ) )
18	17	rspcev	|- ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. y e. RR A. w e. R y <_ w )
19	14 15 18	sylancr	|- ( ph -> E. y e. RR A. w e. R y <_ w )
20		infrecl	|- ( ( R C_ RR /\ R =/= (/) /\ E. y e. RR A. w e. R y <_ w ) -> inf ( R , RR , < ) e. RR )
21	12 13 19 20	syl3anc	|- ( ph -> inf ( R , RR , < ) e. RR )
22	10 21	eqeltrid	|- ( ph -> S e. RR )