Theorem minvec

Description: Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace W that minimizes the distance to an arbitrary vector A in a parent inner product space. Theorem 3.3-1 of Kreyszig p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008) (Proof shortened by Mario Carneiro, 9-May-2014) (Revised by Mario Carneiro, 15-Oct-2015) (Proof shortened 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$$
Assertion	minvec	$$⊢\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		eqid	$$⊢\mathrm{TopOpen}\left(U\right)=\mathrm{TopOpen}\left(U\right)$$
9		oveq2	$$⊢j=y\to A\underset{\dot{}}{-}j=A\underset{\dot{}}{-}y$$
10	9	fveq2d	$$⊢j=y\to N\left(A\underset{\dot{}}{-}j\right)=N\left(A\underset{\dot{}}{-}y\right)$$
11	10	cbvmptv	$$⊢\left(j\in Y⟼N\left(A\underset{\dot{}}{-}j\right)\right)=\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
12	11	rneqi	$$⊢\mathrm{ran}\left(j\in Y⟼N\left(A\underset{\dot{}}{-}j\right)\right)=\mathrm{ran}\left(y\in Y⟼N\left(A\underset{\dot{}}{-}y\right)\right)$$
13		eqid	$$⊢inf\left(\mathrm{ran}\left(j\in Y⟼N\left(A\underset{\dot{}}{-}j\right)\right),ℝ,<\right)=inf\left(\mathrm{ran}\left(j\in Y⟼N\left(A\underset{\dot{}}{-}j\right)\right),ℝ,<\right)$$
14		eqid	$$⊢{\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}={\mathrm{dist}\left(U\right)\upharpoonright }_{\left(X\times X\right)}$$
15	1 2 3 4 5 6 7 8 12 13 14	minveclem7	$$⊢\phi \to \exists !x\in Y\forall y\in YN\left(A\underset{\dot{}}{-}x\right)\le N\left(A\underset{\dot{}}{-}y\right)$$