Theorem minveceu 8542

Description: Minimizing vector 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. Note that we work with the negative of the supremum of negatives instead of infimum in order to use theorems we already have available.

Hypotheses

Ref	Expression
minvec.x	|- X = (Base` U)
minvec.m	|- M = (-v` U)
minvec.n	|- N = (norm` U)
minvec.y	|- Y = (Base` W)
minvec.1	|- R = {x | E.y e. Y x = -u(N` (AMy))}
minvec.2	|- P = -usup(R, RR, < )
minvec.u	|- U e. CPreHil
minvec.w	|- W e. ((SubSp` U) i^i CBan)
minvec.a	|- A e. X

Assertion

Ref	Expression
minveceu	|- E!a e. Y (N` (AMa)) = P

Distinct variable groups:   x,a,y,A   M,a,x,y   N,a,x,y   P,a   R,a   x,U,y   W,a,x,y   Y,a,x,y

Proof of Theorem minveceu

Step	Hyp	Ref	Expression
1		opreq2 3964	. . . . 5 |- (a = b -> (AMa) = (AMb))
2	1	fveq2d 3723	. . . 4 |- (a = b -> (N` (AMa)) = (N` (AMb)))
3	2	eqeq1d 1481	. . 3 |- (a = b -> ((N` (AMa)) = P <-> (N` (AMb)) = P))
4	3	reu4 1931	. 2 |- (E!a e. Y (N` (AMa)) = P <-> (E.a e. Y (N` (AMa)) = P /\ A.a e. Y A.b e. Y (((N` (AMa)) = P /\ (N` (AMb)) = P) -> a = b)))
5		minvec.1	. . 3 |- R = {x | E.y e. Y x = -u(N` (AMy))}
6		minvec.u	. . 3 |- U e. CPreHil
7		minvec.m	. . 3 |- M = (-v` U)
8		minvec.n	. . 3 |- N = (norm` U)
9		minvec.x	. . 3 |- X = (Base` U)
10		minvec.w	. . . 4 |- W e. ((SubSp` U) i^i CBan)
11		inss1 2227	. . . . 5 |- ((SubSp` U) i^i CBan) (_ (SubSp` U)
12	11	sseli 2062	. . . 4 |- (W e. ((SubSp` U) i^i CBan) -> W e. (SubSp` U))
13	10, 12	ax-mp 7	. . 3 |- W e. (SubSp` U)
14		minvec.y	. . 3 |- Y = (Base` W)
15		minvec.a	. . 3 |- A e. X
16		minvec.2	. . 3 |- P = -usup(R, RR, < )
17		fveq2 3719	. . . . . 6 |- (j = n -> (f` j) = (f` n))
18	17	opreq2d 3971	. . . . 5 |- (j = n -> (AM(f` j)) = (AM(f` n)))
19	18	fveq2d 3723	. . . 4 |- (j = n -> (N` (AM(f` j))) = (N` (AM(f` n))))
20		eqid 1474	. . . 4 |- {<.j, v>. | (j e. NN /\ v = (N` (AM(f` j))))} = {<.j, v>. | (j e. NN /\ v = (N` (AM(f` j))))}
21		fvex 3727	. . . 4 |- (N` (AM(f` n))) e. V
22	19, 20, 21	fvopab4 3775	. . 3 |- (n e. NN -> ({<.j, v>. | (j e. NN /\ v = (N` (AM(f` j))))}` n) = (N` (AM(f` n))))
23		eqid 1474	. . 3 |- (IndMet` W) = (IndMet` W)
24		nnex 5891	. . . 4 |- NN e. V
25	24	opabex2 3606	. . 3 |- {<.j, v>. | (j e. NN /\ v = (N` (AM(f` j))))} e. V
26		inss2 2228	. . . . 5 |- ((SubSp` U) i^i CBan) (_ CBan
27	26	sseli 2062	. . . 4 |- (W e. ((SubSp` U) i^i CBan) -> W e. CBan)
28	10, 27	ax-mp 7	. . 3 |- W e. CBan
29	5, 6, 7, 8, 9, 13, 14, 15, 16, 22, 23, 25, 28	minvecex 8537	. 2 |- E.a e. Y (N` (AMa)) = P
30		eqid 1474	. . . . . 6 |- (+v` U) = (+v` U)
31		eqid 1474	. . . . . 6 |- (.s` U) = (.s` U)
32	9, 30, 7, 31, 8, 14, 6, 15, 13, 16, 5	minveclem38 8541	. . . . 5 |- (((a e. Y /\ b e. Y) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> (N` (aMb)) <_ 0)
33	6	phnvi 8434	. . . . . . . . . . 11 |- U e. NrmCVec
34	9, 7	nvmcl 8231	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ a e. X /\ b e. X) -> (aMb) e. X)
35	33, 34	mp3an1 902	. . . . . . . . . 10 |- ((a e. X /\ b e. X) -> (aMb) e. X)
36	9, 8	nvge0 8266	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (aMb) e. X) -> 0 <_ (N` (aMb)))
37	33, 36	mpan 694	. . . . . . . . . 10 |- ((aMb) e. X -> 0 <_ (N` (aMb)))
38	35, 37	syl 10	. . . . . . . . 9 |- ((a e. X /\ b e. X) -> 0 <_ (N` (aMb)))
39		idd 61	. . . . . . . . 9 |- ((a e. X /\ b e. X) -> (((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb))) -> ((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb)))))
40	38, 39	mpan2d 701	. . . . . . . 8 |- ((a e. X /\ b e. X) -> ((N` (aMb)) <_ 0 -> ((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb)))))
41		eqid 1474	. . . . . . . . . . . 12 |- (0v` U) = (0v` U)
42	9, 41, 8	nvz 8261	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ (aMb) e. X) -> ((N` (aMb)) = 0 <-> (aMb) = (0v` U)))
43	33, 42	mpan 694	. . . . . . . . . 10 |- ((aMb) e. X -> ((N` (aMb)) = 0 <-> (aMb) = (0v` U)))
44	35, 43	syl 10	. . . . . . . . 9 |- ((a e. X /\ b e. X) -> ((N` (aMb)) = 0 <-> (aMb) = (0v` U)))
45	9, 8	nvcl 8251	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (aMb) e. X) -> (N` (aMb)) e. RR)
46	33, 45	mpan 694	. . . . . . . . . . 11 |- ((aMb) e. X -> (N` (aMb)) e. RR)
47	35, 46	syl 10	. . . . . . . . . 10 |- ((a e. X /\ b e. X) -> (N` (aMb)) e. RR)
48		0re 5423	. . . . . . . . . . 11 |- 0 e. RR
49		letri3t 5500	. . . . . . . . . . 11 |- (((N` (aMb)) e. RR /\ 0 e. RR) -> ((N` (aMb)) = 0 <-> ((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb)))))
50	48, 49	mpan2 695	. . . . . . . . . 10 |- ((N` (aMb)) e. RR -> ((N` (aMb)) = 0 <-> ((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb)))))
51	47, 50	syl 10	. . . . . . . . 9 |- ((a e. X /\ b e. X) -> ((N` (aMb)) = 0 <-> ((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb)))))
52	9, 7, 41	nvmeq0 8248	. . . . . . . . . 10 |- ((U e. NrmCVec /\ a e. X /\ b e. X) -> ((aMb) = (0v` U) <-> a = b))
53	33, 52	mp3an1 902	. . . . . . . . 9 |- ((a e. X /\ b e. X) -> ((aMb) = (0v` U) <-> a = b))
54	44, 51, 53	3bitr3d 547	. . . . . . . 8 |- ((a e. X /\ b e. X) -> (((N` (aMb)) <_ 0 /\ 0 <_ (N` (aMb))) <-> a = b))
55	40, 54	sylibd 202	. . . . . . 7 |- ((a e. X /\ b e. X) -> ((N` (aMb)) <_ 0 -> a = b))
56	6, 13, 14, 9	minveclem3 8506	. . . . . . . 8 |- Y (_ X
57	56	sseli 2062	. . . . . . 7 |- (a e. Y -> a e. X)
58	56	sseli 2062	. . . . . . 7 |- (b e. Y -> b e. X)
59	55, 57, 58	syl2an 454	. . . . . 6 |- ((a e. Y /\ b e. Y) -> ((N` (aMb)) <_ 0 -> a = b))
60	59	adantr 389	. . . . 5 |- (((a e. Y /\ b e. Y) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> ((N` (aMb)) <_ 0 -> a = b))
61	32, 60	mpd 26	. . . 4 |- (((a e. Y /\ b e. Y) /\ ((N` (AMa)) = P /\ (N` (AMb)) = P)) -> a = b)
62	61	ex 373	. . 3 |- ((a e. Y /\ b e. Y) -> (((N` (AMa)) = P /\ (N` (AMb)) = P) -> a = b))
63	62	rgen2a 1697	. 2 |- A.a e. Y A.b e. Y (((N` (AMa)) = P /\ (N` (AMb)) = P) -> a = b)
64	4, 29, 63	mpbir2an 729	1 |- E!a e. Y (N` (AMa)) = P

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 955   e. wcel 957  {cab 1462  A.wral 1643  E.wrex 1644  E!wreu 1645   i^i cin 2043   class class class wbr 2615  {copab 2662  ` cfv 3178  (class class class)co 3958  supcsup 4556  RRcr 5216  0cc0 5217  -ucneg 5276   <_ cle 5278  NNcn 5279   < clt 5469  NrmCVeccnv 8167  +vcpv 8168  Basecba 8169  .scns 8170  0vcn0v 8171  -vcnsb 8172  normcnm 8173  IndMetcims 8174  SubSpcss 8342  CPreHilcphl 8430  CBancbn 8481

This theorem is referenced by:  minveccl 8543  minvecdist 8544

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862  ax-reg 4576  ax-inf2 4608  ax-ac 4727

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-nel 1586  df-ral 1647  df-rex 1648  df-reu 1649  df-rab 1650  df-v 1809  df-sbc 1939  df-csb 1999  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-pss 2052  df-nul 2278  df-if 2359  df-pw 2399  df-sn 2409  df-pr 2410  df-tp 2412  df-op 2413  df-uni 2500  df-int 2530  df-iun 2564  df-iin 2565  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2828  df-id 2831  df-po 2836  df-so 2846  df-fr 2913  df-we 2930  df-ord 2947  df-on 2948  df-lim 2949  df-suc 2950  df-om 3128  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185