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 = ( 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 )
Assertion	minvec	|- ( ph -> E! x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )

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		eqid	|- ( TopOpen ` U ) = ( TopOpen ` U )
9		oveq2	|- ( j = y -> ( A .- j ) = ( A .- y ) )
10	9	fveq2d	|- ( j = y -> ( N ` ( A .- j ) ) = ( N ` ( A .- y ) ) )
11	10	cbvmptv	|- ( j e. Y |-> ( N ` ( A .- j ) ) ) = ( y e. Y |-> ( N ` ( A .- y ) ) )
12	11	rneqi	|- ran ( j e. Y |-> ( N ` ( A .- j ) ) ) = ran ( y e. Y |-> ( N ` ( A .- y ) ) )
13		eqid	|- inf ( ran ( j e. Y |-> ( N ` ( A .- j ) ) ) , RR , < ) = inf ( ran ( j e. Y |-> ( N ` ( A .- j ) ) ) , RR , < )
14		eqid	|- ( ( dist ` U ) |` ( X X. X ) ) = ( ( dist ` U ) |` ( X X. X ) )
15	1 2 3 4 5 6 7 8 12 13 14	minveclem7	|- ( ph -> E! x e. Y A. y e. Y ( N ` ( A .- x ) ) <_ ( N ` ( A .- y ) ) )