This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ X = BaseSet ⁡ U
minveco.m ⊢ M = - v ⁡ U
minveco.n ⊢ N = norm CV ⁡ U
minveco.y ⊢ Y = BaseSet ⁡ W
minveco.u ⊢ φ → U ∈ CPreHil OLD
minveco.w ⊢ φ → W ∈ SubSp ⁡ U ∩ CBan
minveco.a ⊢ φ → A ∈ X
Assertion minveco ⊢ φ → ∃! x ∈ Y ∀ y ∈ Y N ⁡ A M x ≤ N ⁡ A M y

Proof

Step Hyp Ref Expression
1 minveco.x ⊢ X = BaseSet ⁡ U
2 minveco.m ⊢ M = - v ⁡ U
3 minveco.n ⊢ N = norm CV ⁡ U
4 minveco.y ⊢ Y = BaseSet ⁡ W
5 minveco.u ⊢ φ → U ∈ CPreHil OLD
6 minveco.w ⊢ φ → W ∈ SubSp ⁡ U ∩ CBan
7 minveco.a ⊢ φ → A ∈ X
8 eqid ⊢ IndMet ⁡ U = IndMet ⁡ U
9 eqid ⊢ MetOpen ⁡ IndMet ⁡ U = MetOpen ⁡ IndMet ⁡ U
10 oveq2 ⊢ j = y → A M j = A M y
11 10 fveq2d ⊢ j = y → N ⁡ A M j = N ⁡ A M y
12 11 cbvmptv ⊢ j ∈ Y ⟼ N ⁡ A M j = y ∈ Y ⟼ N ⁡ A M y
13 12 rneqi ⊢ ran ⁡ j ∈ Y ⟼ N ⁡ A M j = ran ⁡ y ∈ Y ⟼ N ⁡ A M y
14 eqid ⊢ inf ran ⁡ j ∈ Y ⟼ N ⁡ A M j ℝ < = inf ran ⁡ j ∈ Y ⟼ N ⁡ A M j ℝ <
15 1 2 3 4 5 6 7 8 9 13 14 minvecolem7 ⊢ φ → ∃! x ∈ Y ∀ y ∈ Y N ⁡ A M x ≤ N ⁡ A M y