Theorem minveclem4b

Description: Lemma for minvec . The convergent point of the Cauchy sequence F is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by Mario Carneiro, 15-Oct-2015)

	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)$$
	minvec.d	$$⊢D={\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}$$
	minvec.f	$$⊢F=\mathrm{ran}\left(r\in {ℝ}^{+}⟼\left\{y\in Y|{\left(ADy\right)}^2\le S^2+r\right\}\right)$$
	minvec.p	$$⊢P=\bigcup \left(J\mathrm{fLim}\left(X\mathrm{filGen}F\right)\right)$$
Assertion	minveclem4b	$$⊢\phi \to P\in X$$

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		minvec.d	$$⊢D={\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}$$
12		minvec.f	$$⊢F=\mathrm{ran}\left(r\in {ℝ}^{+}⟼\left\{y\in Y|{\left(ADy\right)}^2\le S^2+r\right\}\right)$$
13		minvec.p	$$⊢P=\bigcup \left(J\mathrm{fLim}\left(X\mathrm{filGen}F\right)\right)$$
14		eqid	$$⊢\mathrm{LSubSp}\left(U\right)=\mathrm{LSubSp}\left(U\right)$$
15	1 14	lssss	$$⊢Y\in \mathrm{LSubSp}\left(U\right)\to Y\subseteq X$$
16	5 15	syl	$$⊢\phi \to Y\subseteq X$$
17	1 2 3 4 5 6 7 8 9 10 11 12 13	minveclem4a	$$⊢\phi \to P\in \left(\left(J\mathrm{fLim}\left(X\mathrm{filGen}F\right)\right)\cap Y\right)$$
18	17	elin2d	$$⊢\phi \to P\in Y$$
19	16 18	sseldd	$$⊢\phi \to P\in X$$