Theorem minveco

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
	minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
	minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion	minveco	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5		minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6		minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7		minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		eqid	⊢ ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 )
9		eqid	⊢ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) = ( MetOpen ‘ ( IndMet ‘ 𝑈 ) )
10		oveq2	⊢ ( 𝑗 = 𝑦 → ( 𝐴 𝑀 𝑗 ) = ( 𝐴 𝑀 𝑦 ) )
11	10	fveq2d	⊢ ( 𝑗 = 𝑦 → ( 𝑁 ‘ ( 𝐴 𝑀 𝑗 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
12	11	cbvmptv	⊢ ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑗 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
13	12	rneqi	⊢ ran ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑗 ) ) ) = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
14		eqid	⊢ inf ( ran ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑗 ) ) ) , ℝ , < ) = inf ( ran ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑗 ) ) ) , ℝ , < )
15	1 2 3 4 5 6 7 8 9 13 14	minvecolem7	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )