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	$⊢ φ \to U \in {CPreHil}_{OLD}$
	minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
	minveco.a	$⊢ φ \to A \in X$
Assertion	minveco	$⊢ φ \to \exists! x \in Y \forall y \in Y N (A M x) \leq 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	$⊢ φ \to U \in {CPreHil}_{OLD}$
6		minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
7		minveco.a	$⊢ φ \to A \in X$
8		eqid	$⊢ IndMet (U) = IndMet (U)$
9		eqid	$⊢ MetOpen (IndMet (U)) = MetOpen (IndMet (U))$
10		oveq2	$⊢ j = y \to A M j = A M y$
11	10	fveq2d	$⊢ j = y \to N (A M j) = N (A M y)$
12	11	cbvmptv	$⊢ (j \in Y ⟼ N (A M j)) = (y \in Y ⟼ N (A M y))$
13	12	rneqi	$⊢ ran (j \in Y ⟼ N (A M j)) = ran (y \in Y ⟼ N (A M y))$
14		eqid	$⊢ sup (ran (j \in Y ⟼ N (A M j)) ℝ <) = sup (ran (j \in Y ⟼ N (A M j)) ℝ <)$
15	1 2 3 4 5 6 7 8 9 13 14	minvecolem7	$⊢ φ \to \exists! x \in Y \forall y \in Y N (A M x) \leq N (A M y)$

Metamath Proof Explorer

Theorem minveco

Proof