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 = ( normCV ` U ) |
||
| minveco.y | |- Y = ( BaseSet ` W ) |
||
| minveco.u | |- ( ph -> U e. CPreHilOLD ) |
||
| minveco.w | |- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) ) |
||
| minveco.a | |- ( ph -> A e. X ) |
||
| Assertion | minveco | |- ( ph -> E! x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | minveco.x | |- X = ( BaseSet ` U ) |
|
| 2 | minveco.m | |- M = ( -v ` U ) |
|
| 3 | minveco.n | |- N = ( normCV ` U ) |
|
| 4 | minveco.y | |- Y = ( BaseSet ` W ) |
|
| 5 | minveco.u | |- ( ph -> U e. CPreHilOLD ) |
|
| 6 | minveco.w | |- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) ) |
|
| 7 | minveco.a | |- ( ph -> A e. 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 e. Y |-> ( N ` ( A M j ) ) ) = ( y e. Y |-> ( N ` ( A M y ) ) ) |
| 13 | 12 | rneqi | |- ran ( j e. Y |-> ( N ` ( A M j ) ) ) = ran ( y e. Y |-> ( N ` ( A M y ) ) ) |
| 14 | eqid | |- inf ( ran ( j e. Y |-> ( N ` ( A M j ) ) ) , RR , < ) = inf ( ran ( j e. Y |-> ( N ` ( A M j ) ) ) , RR , < ) |
|
| 15 | 1 2 3 4 5 6 7 8 9 13 14 | minvecolem7 | |- ( ph -> E! x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) ) |