Theorem minveclem5

Description: Lemma for minvec . Discharge the assumptions in minveclem4 . (Contributed by Mario Carneiro, 9-May-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)}$$
Assertion	minveclem5	$$⊢\phi \to \exists x\in Y\forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)$$

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		oveq2	$$⊢s=r\to S^2+s=S^2+r$$
13	12	breq2d	$$⊢s=r\to \left({\left(ADz\right)}^2\le S^2+s\leftrightarrow {\left(ADz\right)}^2\le S^2+r\right)$$
14	13	rabbidv	$$⊢s=r\to \left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}=\left\{z\in Y|{\left(ADz\right)}^2\le S^2+r\right\}$$
15		oveq2	$$⊢z=y\to ADz=ADy$$
16	15	oveq1d	$$⊢z=y\to {\left(ADz\right)}^2={\left(ADy\right)}^2$$
17	16	breq1d	$$⊢z=y\to \left({\left(ADz\right)}^2\le S^2+r\leftrightarrow {\left(ADy\right)}^2\le S^2+r\right)$$
18	17	cbvrabv	$$⊢\left\{z\in Y|{\left(ADz\right)}^2\le S^2+r\right\}=\left\{y\in Y|{\left(ADy\right)}^2\le S^2+r\right\}$$
19	14 18	eqtrdi	$$⊢s=r\to \left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}=\left\{y\in Y|{\left(ADy\right)}^2\le S^2+r\right\}$$
20	19	cbvmptv	$$⊢\left(s\in {ℝ}^{+}⟼\left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}\right)=\left(r\in {ℝ}^{+}⟼\left\{y\in Y|{\left(ADy\right)}^2\le S^2+r\right\}\right)$$
21	20	rneqi	$$⊢\mathrm{ran}\left(s\in {ℝ}^{+}⟼\left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}\right)=\mathrm{ran}\left(r\in {ℝ}^{+}⟼\left\{y\in Y|{\left(ADy\right)}^2\le S^2+r\right\}\right)$$
22		eqid	$$⊢\bigcup \left(J\mathrm{fLim}\left(X\mathrm{filGen}\mathrm{ran}\left(s\in {ℝ}^{+}⟼\left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}\right)\right)\right)=\bigcup \left(J\mathrm{fLim}\left(X\mathrm{filGen}\mathrm{ran}\left(s\in {ℝ}^{+}⟼\left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}\right)\right)\right)$$
23		eqid	$$⊢{\left(\frac{\left(AD\bigcup \left(J\mathrm{fLim}\left(X\mathrm{filGen}\mathrm{ran}\left(s\in {ℝ}^{+}⟼\left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}\right)\right)\right)\right)+S}{2}\right)}^2-S^2={\left(\frac{\left(AD\bigcup \left(J\mathrm{fLim}\left(X\mathrm{filGen}\mathrm{ran}\left(s\in {ℝ}^{+}⟼\left\{z\in Y|{\left(ADz\right)}^2\le S^2+s\right\}\right)\right)\right)\right)+S}{2}\right)}^2-S^2$$
24	1 2 3 4 5 6 7 8 9 10 11 21 22 23	minveclem4	$$⊢\phi \to \exists x\in Y\forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)$$