Theorem htthlem6 8555

Description: Lemma for htthi 8562. An upper bound of all F` k at a given vector A, when the norms of auxiliary vector sequence f are all 1 or less.

Hypotheses

Ref	Expression
htthlem3.1	|- X = (Base` U)
htthlem3.p	|- P = (.i` U)
htthlem3.l	|- L = (U LnOp U)
htthlem3.b	|- B = (U BLnOp U)
htthlem3.u	|- U e. CHil
htthlem3.t	|- T e. L
htthlem3.a	|- ((x e. X /\ y e. X) -> ((T` x)Py) = (xP(T` y)))
htthlem3.f	|- F = {<.m, w>. | (m e. NN /\ w = {<.v, u>. | (v e. X /\ u = ((T` v)P(f` m)))})}
htthlem3.c	|- C = <.<. + , x. >., abs>.
htthlem3.d	|- D = (U BLnOp C)
htthlem3.n	|- N = (norm` U)
htthlem3.o	|- O = (UnormOpC)

Assertion

Ref	Expression
htthlem6	|- (((A e. X /\ (f:NN-->X /\ k e. NN)) /\ (N` (f` k)) <_ 1) -> (abs` ((F` k)` A)) <_ (N` (T` A)))

Distinct variable groups:   v,u,x,y,A   C,k   D,k   k,F   f,k,N   u,m,v,w,x,y,P   u,k,v,x,y   f,m,u,v,w,x,y,T,k   U,k,u,v   f,X,k,m,u,v,w,x,y

Proof of Theorem htthlem6

Step	Hyp	Ref	Expression
1		htthlem3.1	. . . . . 6 |- X = (Base` U)
2		htthlem3.p	. . . . . 6 |- P = (.i` U)
3		htthlem3.l	. . . . . 6 |- L = (U LnOp U)
4		htthlem3.b	. . . . . 6 |- B = (U BLnOp U)
5		htthlem3.u	. . . . . 6 |- U e. CHil
6		htthlem3.t	. . . . . 6 |- T e. L
7		htthlem3.a	. . . . . 6 |- ((x e. X /\ y e. X) -> ((T` x)Py) = (xP(T` y)))
8		htthlem3.f	. . . . . 6 |- F = {<.m, w>. | (m e. NN /\ w = {<.v, u>. | (v e. X /\ u = ((T` v)P(f` m)))})}
9		htthlem3.c	. . . . . 6 |- C = <.<. + , x. >., abs>.
10		htthlem3.d	. . . . . 6 |- D = (U BLnOp C)
11		htthlem3.n	. . . . . 6 |- N = (norm` U)
12		htthlem3.o	. . . . . 6 |- O = (UnormOpC)
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	htthlem4 8553	. . . . 5 |- ((A e. X /\ k e. NN) -> ((F` k)` A) = ((T` A)P(f` k)))
14	13	fveq2d 3713	. . . 4 |- ((A e. X /\ k e. NN) -> (abs` ((F` k)` A)) = (abs` ((T` A)P(f` k))))
15	14	adantrl 394	. . 3 |- ((A e. X /\ (f:NN-->X /\ k e. NN)) -> (abs` ((F` k)` A)) = (abs` ((T` A)P(f` k))))
16	15	adantr 389	. 2 |- (((A e. X /\ (f:NN-->X /\ k e. NN)) /\ (N` (f` k)) <_ 1) -> (abs` ((F` k)` A)) = (abs` ((T` A)P(f` k))))
17	5	hlnvi 8527	. . . . . . 7 |- U e. NrmCVec
18	1, 2	ipcl 8299	. . . . . . 7 |- ((U e. NrmCVec /\ (T` A) e. X /\ (f` k) e. X) -> ((T` A)P(f` k)) e. CC)
19	17, 18	mp3an1 900	. . . . . 6 |- (((T` A) e. X /\ (f` k) e. X) -> ((T` A)P(f` k)) e. CC)
20		absclt 6768	. . . . . 6 |- (((T` A)P(f` k)) e. CC -> (abs` ((T` A)P(f` k))) e. RR)
21	19, 20	syl 10	. . . . 5 |- (((T` A) e. X /\ (f` k) e. X) -> (abs` ((T` A)P(f` k))) e. RR)
22	21	adantr 389	. . . 4 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> (abs` ((T` A)P(f` k))) e. RR)
23		axmulrcl 5246	. . . . . 6 |- (((N` (T` A)) e. RR /\ (N` (f` k)) e. RR) -> ((N` (T` A)) x. (N` (f` k))) e. RR)
24	1, 11	nvcl 8227	. . . . . . 7 |- ((U e. NrmCVec /\ (T` A) e. X) -> (N` (T` A)) e. RR)
25	17, 24	mpan 693	. . . . . 6 |- ((T` A) e. X -> (N` (T` A)) e. RR)
26	1, 11	nvcl 8227	. . . . . . 7 |- ((U e. NrmCVec /\ (f` k) e. X) -> (N` (f` k)) e. RR)
27	17, 26	mpan 693	. . . . . 6 |- ((f` k) e. X -> (N` (f` k)) e. RR)
28	23, 25, 27	syl2an 454	. . . . 5 |- (((T` A) e. X /\ (f` k) e. X) -> ((N` (T` A)) x. (N` (f` k))) e. RR)
29	28	adantr 389	. . . 4 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> ((N` (T` A)) x. (N` (f` k))) e. RR)
30	25	ad2antrr 404	. . . 4 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> (N` (T` A)) e. RR)
31		hlph 8524	. . . . . . 7 |- (U e. CHil -> U e. CPreHil)
32	5, 31	ax-mp 7	. . . . . 6 |- U e. CPreHil
33	1, 11, 2, 32	sii 8445	. . . . 5 |- (((T` A) e. X /\ (f` k) e. X) -> (abs` ((T` A)P(f` k))) <_ ((N` (T` A)) x. (N` (f` k))))
34	33	adantr 389	. . . 4 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> (abs` ((T` A)P(f` k))) <_ ((N` (T` A)) x. (N` (f` k))))
35		1re 5407	. . . . . . 7 |- 1 e. RR
36		lemul2it 5795	. . . . . . 7 |- ((((N` (f` k)) e. RR /\ 1 e. RR /\ ((N` (T` A)) e. RR /\ 0 <_ (N` (T` A)))) /\ (N` (f` k)) <_ 1) -> ((N` (T` A)) x. (N` (f` k))) <_ ((N` (T` A)) x. 1))
37	35, 36	mp3anl2 908	. . . . . 6 |- ((((N` (f` k)) e. RR /\ ((N` (T` A)) e. RR /\ 0 <_ (N` (T` A)))) /\ (N` (f` k)) <_ 1) -> ((N` (T` A)) x. (N` (f` k))) <_ ((N` (T` A)) x. 1))
38	1, 11	nvge0 8241	. . . . . . . . . 10 |- ((U e. NrmCVec /\ (T` A) e. X) -> 0 <_ (N` (T` A)))
39	17, 38	mpan 693	. . . . . . . . 9 |- ((T` A) e. X -> 0 <_ (N` (T` A)))
40	25, 39	jca 288	. . . . . . . 8 |- ((T` A) e. X -> ((N` (T` A)) e. RR /\ 0 <_ (N` (T` A))))
41	27, 40	anim12i 333	. . . . . . 7 |- (((f` k) e. X /\ (T` A) e. X) -> ((N` (f` k)) e. RR /\ ((N` (T` A)) e. RR /\ 0 <_ (N` (T` A)))))
42	41	ancoms 436	. . . . . 6 |- (((T` A) e. X /\ (f` k) e. X) -> ((N` (f` k)) e. RR /\ ((N` (T` A)) e. RR /\ 0 <_ (N` (T` A)))))
43	37, 42	sylan 448	. . . . 5 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> ((N` (T` A)) x. (N` (f` k))) <_ ((N` (T` A)) x. 1))
44	25	recnd 5287	. . . . . . 7 |- ((T` A) e. X -> (N` (T` A)) e. CC)
45		ax1id 5254	. . . . . . 7 |- ((N` (T` A)) e. CC -> ((N` (T` A)) x. 1) = (N` (T` A)))
46	44, 45	syl 10	. . . . . 6 |- ((T` A) e. X -> ((N` (T` A)) x. 1) = (N` (T` A)))
47	46	ad2antrr 404	. . . . 5 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> ((N` (T` A)) x. 1) = (N` (T` A)))
48	43, 47	breqtrd 2629	. . . 4 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> ((N` (T` A)) x. (N` (f` k))) <_ (N` (T` A)))
49	22, 29, 30, 34, 48	letrd 5499	. . 3 |- ((((T` A) e. X /\ (f` k) e. X) /\ (N` (f` k)) <_ 1) -> (abs` ((T` A)P(f` k))) <_ (N` (T` A)))
50	1, 1, 3	lnof 8350	. . . . . 6 |- ((U e. NrmCVec /\ U e. NrmCVec /\ T e. L) -> T:X-->X)
51	17, 17, 6, 50	mp3an 913	. . . . 5 |- T:X-->X
52	51	ffvelrni 3800	. . . 4 |- (A e. X -> (T` A) e. X)
53		ffvelrn 3799	. . . 4 |- ((f:NN-->X /\