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={\mathrm{Base}}_U$$
	minvec.m	$$⊢\underset{\dot{}}{-}={-}_U$$
	minvec.n	$$⊢N=\mathrm{norm}\left(U\right)$$
	minvec.u	$$⊢\phi \to U\in \mathrm{CPreHil}$$
	minvec.y	$$⊢\phi \to Y\in \mathrm{LSubSp}\left(U\right)$$
	minvec.w	$$⊢\phi \to U{\upharpoonright }_{𝑠}Y\in \mathrm{CMetSp}$$
	minvec.a	$$⊢\phi \to A\in X$$
	minvec.j	$$⊢J=\mathrm{TopOpen}\left(U\right)$$
	minvec.r	$$⊢R=\mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
	minvec.s	$$⊢S=inf\left(R,ℝ,<\right)$$
Assertion	minveclem4c	$$⊢\phi \to S\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		minvec.x	$$⊢X={\mathrm{Base}}_U$$
2		minvec.m	$$⊢\underset{\dot{}}{-}={-}_U$$
3		minvec.n	$$⊢N=\mathrm{norm}\left(U\right)$$
4		minvec.u	$$⊢\phi \to U\in \mathrm{CPreHil}$$
5		minvec.y	$$⊢\phi \to Y\in \mathrm{LSubSp}\left(U\right)$$
6		minvec.w	$$⊢\phi \to U{\upharpoonright }_{𝑠}Y\in \mathrm{CMetSp}$$
7		minvec.a	$$⊢\phi \to A\in X$$
8		minvec.j	$$⊢J=\mathrm{TopOpen}\left(U\right)$$
9		minvec.r	$$⊢R=\mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
10		minvec.s	$$⊢S=inf\left(R,ℝ,<\right)$$
11	1 2 3 4 5 6 7 8 9	minveclem1	$$⊢\phi \to \left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \forall w\in R0\le w\right)$$
12	11	simp1d	$$⊢\phi \to R\subseteq ℝ$$
13	11	simp2d	$$⊢\phi \to R\ne \varnothing$$
14		0re	$$⊢0\in ℝ$$
15	11	simp3d	$$⊢\phi \to \forall w\in R0\le w$$
16		breq1	$$⊢y=0\to \left(y\le w\leftrightarrow 0\le w\right)$$
17	16	ralbidv	$$⊢y=0\to \left(\forall w\in Ry\le w\leftrightarrow \forall w\in R0\le w\right)$$
18	17	rspcev	$$⊢\left(0\in ℝ\wedge \forall w\in R0\le w\right)\to \exists y\in ℝ\forall w\in Ry\le w$$
19	14 15 18	sylancr	$$⊢\phi \to \exists y\in ℝ\forall w\in Ry\le w$$
20		infrecl	$$⊢\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists y\in ℝ\forall w\in Ry\le w\right)\to inf\left(R,ℝ,<\right)\in ℝ$$
21	12 13 19 20	syl3anc	$$⊢\phi \to inf\left(R,ℝ,<\right)\in ℝ$$
22	10 21	eqeltrid	$$⊢\phi \to S\in ℝ$$