Theorem minveclem28 8580

Description: Lemma for minvecex 8586.

Hypotheses

Ref	Expression
minvec10.1	|- R = {x | E.y e. Y x = -u(N` (AMy))}
minvec10.u	|- U e. CPreHil
minvec10.m	|- M = (-v` U)
minvec10.n	|- N = (norm` U)
minvec10.x	|- X = (Base` U)
minvec10.w1	|- W e. (SubSp` U)
minvec10.y	|- Y = (Base` W)
minvec10.a	|- A e. X
minvec22.hf	|- (j e. NN -> (F` j) = (N` (AM(f` j))))
minvec23.2	|- P = -usup(R, RR, < )
minvec28.d	|- D = (IndMet` W)

Assertion

Ref	Expression
minveclem28	|- (((f:NN-->Y /\ F ~~> P) /\ B e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> ((f` k)D(f` m)) < B))

Distinct variable groups:   f,j,k,m,x,y,A   B,k,m,x,y   D,k,m   j,F,k,m   f,M,j,k,m,x,y   f,N,j,k,m,x,y   P,f,j,k,m   x,U,y   x,W,y   f,Y,j,k,m,x,y   x,P,y

Proof of Theorem minveclem28

Step	Hyp	Ref	Expression
1		minvec10.1	. . . 4 |- R = {x | E.y e. Y x = -u(N` (AMy))}
2		minvec10.u	. . . 4 |- U e. CPreHil
3		minvec10.m	. . . 4 |- M = (-v` U)
4		minvec10.n	. . . 4 |- N = (norm` U)
5		minvec10.x	. . . 4 |- X = (Base` U)
6		minvec10.w1	. . . 4 |- W e. (SubSp` U)
7		minvec10.y	. . . 4 |- Y = (Base` W)
8		minvec10.a	. . . 4 |- A e. X
9		minvec22.hf	. . . 4 |- (j e. NN -> (F` j) = (N` (AM(f` j))))
10		minvec23.2	. . . 4 |- P = -usup(R, RR, < )
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem27 8579	. . 3 |- (((f:NN-->Y /\ F ~~> P) /\ (B^2) e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> ((N` ((f` k)M(f` m)))^2) < (B^2)))
12		2nn0 6121	. . . 4 |- 2 e. NN0
13		rpexpclt 6595	. . . 4 |- ((B e. RR+ /\ 2 e. NN0) -> (B^2) e. RR+)
14	12, 13	mpan2 700	. . 3 |- (B e. RR+ -> (B^2) e. RR+)
15	11, 14	sylan2 454	. 2 |- (((f:NN-->Y /\ F ~~> P) /\ B e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> ((N` ((f` k)M(f` m)))^2) < (B^2)))
16	2	phnvi 8483	. . . . . . . . . . . . . . 15 |- U e. NrmCVec
17		eqid 1482	. . . . . . . . . . . . . . . 16 |- (SubSp` U) = (SubSp` U)
18	17	sspnv 8393	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ W e. (SubSp` U)) -> W e. NrmCVec)
19	16, 6, 18	mp2an 701	. . . . . . . . . . . . . 14 |- W e. NrmCVec
20		eqid 1482	. . . . . . . . . . . . . . 15 |- (-v` W) = (-v` W)
21		eqid 1482	. . . . . . . . . . . . . . 15 |- (norm` W) = (norm` W)
22		minvec28.d	. . . . . . . . . . . . . . 15 |- D = (IndMet` W)
23	7, 20, 21, 22	imsdval 8325	. . . . . . . . . . . . . 14 |- ((W e. NrmCVec /\ (f` k) e. Y /\ (f` m) e. Y) -> ((f` k)D(f` m)) = ((norm` W)` ((f` k)(-v` W)(f` m))))
24	19, 23	mp3an1 907	. . . . . . . . . . . . 13 |- (((f` k) e. Y /\ (f` m) e. Y) -> ((f` k)D(f` m)) = ((norm` W)` ((f` k)(-v` W)(f` m))))
25	7, 20	nvmcl 8275	. . . . . . . . . . . . . . 15 |- ((W e. NrmCVec /\ (f` k) e. Y /\ (f` m) e. Y) -> ((f` k)(-v` W)(f` m)) e. Y)
26	19, 25	mp3an1 907	. . . . . . . . . . . . . 14 |- (((f` k) e. Y /\ (f` m) e. Y) -> ((f` k)(-v` W)(f` m)) e. Y)
27	7, 4, 21, 17	sspnval 8404	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ W e. (SubSp` U) /\ ((f` k)(-v` W)(f` m)) e. Y) -> ((norm` W)` ((f` k)(-v` W)(f` m))) = (N` ((f` k)(-v` W)(f` m))))
28	16, 6, 27	mp3an12 910	. . . . . . . . . . . . . 14 |- (((f` k)(-v` W)(f` m)) e. Y -> ((norm` W)` ((f` k)(-v` W)(f` m))) = (N` ((f` k)(-v` W)(f` m))))
29	26, 28	syl 10	. . . . . . . . . . . . 13 |- (((f` k) e. Y /\ (f` m) e. Y) -> ((norm` W)` ((f` k)(-v` W)(f` m))) = (N` ((f` k)(-v` W)(f` m))))
30	7, 3, 20, 17	sspmval 8400	. . . . . . . . . . . . . . 15 |- (((U e. NrmCVec /\ W e. (SubSp` U)) /\ ((f` k) e. Y /\ (f` m) e. Y)) -> ((f` k)(-v` W)(f` m)) = ((f` k)M(f` m)))
31	16, 6, 30	mpanl12 712	. . . . . . . . . . . . . 14 |- (((f` k) e. Y /\ (f` m) e. Y) -> ((f` k)(-v` W)(f` m)) = ((f` k)M(f` m)))
32	31	fveq2d 3742	. . . . . . . . . . . . 13 |- (((f` k) e. Y /\ (f` m) e. Y) -> (N` ((f` k)(-v` W)(f` m))) = (N` ((f` k)M(f` m))))
33	24, 29, 32	3eqtrd 1518	. . . . . . . . . . . 12 |- (((f` k) e. Y /\ (f` m) e. Y) -> ((f` k)D(f` m)) = (N` ((f` k)M(f` m))))
34	33	adantr 391	. . . . . . . . . . 11 |- ((((f` k) e. Y /\ (f` m) e. Y) /\ B e. RR+) -> ((f` k)D(f` m)) = (N` ((f` k)M(f` m))))
35	34	breq1d 2642	. . . . . . . . . 10 |- ((((f` k) e. Y /\ (f` m) e. Y) /\ B e. RR+) -> (((f` k)D(f` m)) < B <-> (N` ((f` k)M(f` m))) < B))
36		lt2sqt 6643	. . . . . . . . . . 11 |- ((((N` ((f` k)M(f` m))) e. RR /\ 0 <_ (N` ((f` k)M(f` m)))) /\ (B e. RR /\ 0 <_ B)) -> ((N` ((f` k)M(f` m))) < B <-> ((N` ((f` k)M(f` m)))^2) < (B^2)))
37	5, 3	nvmcl 8275	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ (f` k) e. X /\ (f` m) e. X) -> ((f` k)M(f` m)) e. X)
38	16, 37	mp3an1 907	. . . . . . . . . . . . 13 |- (((f` k) e. X /\ (f` m) e. X) -> ((f` k)M(f` m)) e. X)
39	5, 4	nvcl 8295	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ ((f` k)M(f` m)) e. X) -> (N` ((f` k)M(f` m))) e. RR)
40	16, 39	mpan 699	. . . . . . . . . . . . . 14 |- (((f` k)M(f` m)) e. X -> (N` ((f` k)M(f` m))) e. RR)
41	5, 4	nvge0 8310	. . . . . . . . . . . . . . 15 |- ((U e. NrmCVec /\ ((f` k)M(f` m)) e. X) -> 0 <_ (N` ((f` k)M(f` m))))
42	16, 41	mpan 699	. . . . . . . . . . . . . 14 |- (((f` k)M(f` m)) e. X -> 0 <_ (N` ((f` k)M(f` m))))
43	40, 42	jca 288	. . . . . . . . . . . . 13 |- (((f` k)M(f` m)) e. X -> ((N` ((f` k)M(f` m))) e. RR /\ 0 <_ (N` ((f` k)M(f` m)))))
44	38, 43	syl 10	. . . . . . . . . . . 12 |- (((f` k) e. X /\ (f` m) e. X) -> ((N` ((f` k)M(f` m))) e. RR /\ 0 <_ (N` ((f` k)M(f` m)))))
45	5, 7, 17	sspba 8394	. . . . . . . . . . . . . 14 |- ((U e. NrmCVec /\ W e. (SubSp` U)) -> Y (_ X)
46	16, 6, 45	mp2an 701	. . . . . . . . . . . . 13 |- Y (_ X
47	46	sseli 2074	. . . . . . . . . . . 12 |- ((f` k) e. Y -> (f` k) e. X)
48	46	sseli 2074	. . . . . . . . . . . 12 |- ((f` m) e. Y -> (f` m) e. X)
49	44, 47, 48	syl2an 457	. . . . . . . . . . 11 |- (((f` k) e. Y /\ (f` m) e. Y) -> ((N` ((f` k)M(f` m))) e. RR /\ 0 <_ (N` ((f` k)M(f` m)))))
50		rpret 6295	. . . . . . . . . . . 12 |- (B e. RR+ -> B e. RR)
51		rpge0t 6298	. . . . . . . . . . . 12 |- (B e. RR+ -> 0 <_ B)
52	50, 51	jca 288	. . . . . . . . . . 11 |- (B e. RR+ -> (B e. RR /\ 0 <_ B))
53	36, 49, 52	syl2an 457	. . . . . . . . . 10 |- ((((f` k) e. Y /\ (f` m) e. Y) /\ B e. RR+) -> ((N` ((f` k)M(f` m))) < B <-> ((N` ((f` k)M(f` m)))^2) < (B^2)))
54	35, 53	bitr2d 532	. . . . . . . . 9 |- ((((f` k) e. Y /\ (f` m) e. Y) /\ B e.