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	⊢ 𝑋 = ( Base ‘ 𝑈 )
	minvec.m	⊢ − = ( -g ‘ 𝑈 )
	minvec.n	⊢ 𝑁 = ( norm ‘ 𝑈 )
	minvec.u	⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
	minvec.y	⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
	minvec.w	⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
	minvec.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion	minvec	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		minvec.x	⊢ 𝑋 = ( Base ‘ 𝑈 )
2		minvec.m	⊢ − = ( -g ‘ 𝑈 )
3		minvec.n	⊢ 𝑁 = ( norm ‘ 𝑈 )
4		minvec.u	⊢ ( 𝜑 → 𝑈 ∈ ℂPreHil )
5		minvec.y	⊢ ( 𝜑 → 𝑌 ∈ ( LSubSp ‘ 𝑈 ) )
6		minvec.w	⊢ ( 𝜑 → ( 𝑈 ↾s 𝑌 ) ∈ CMetSp )
7		minvec.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		eqid	⊢ ( TopOpen ‘ 𝑈 ) = ( TopOpen ‘ 𝑈 )
9		oveq2	⊢ ( 𝑗 = 𝑦 → ( 𝐴 − 𝑗 ) = ( 𝐴 − 𝑦 ) )
10	9	fveq2d	⊢ ( 𝑗 = 𝑦 → ( 𝑁 ‘ ( 𝐴 − 𝑗 ) ) = ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
11	10	cbvmptv	⊢ ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑗 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
12	11	rneqi	⊢ ran ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑗 ) ) ) = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )
13		eqid	⊢ inf ( ran ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑗 ) ) ) , ℝ , < ) = inf ( ran ( 𝑗 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 − 𝑗 ) ) ) , ℝ , < )
14		eqid	⊢ ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑈 ) ↾ ( 𝑋 × 𝑋 ) )
15	1 2 3 4 5 6 7 8 12 13 14	minveclem7	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 − 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 − 𝑦 ) ) )