Theorem htthlem10 8625

Description: Lemma for htthi 8628.

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
htthlem10	|- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> (N` (T` (f` k))) <_ d)

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

Proof of Theorem htthlem10

Step	Hyp	Ref	Expression
1		htthlem3.1	. . . . 5 |- X = (Base` U)
2		htthlem3.p	. . . . 5 |- P = (.i` U)
3		htthlem3.l	. . . . 5 |- L = (U LnOp U)
4		htthlem3.b	. . . . 5 |- B = (U BLnOp U)
5		htthlem3.u	. . . . 5 |- U e. CHil
6		htthlem3.t	. . . . 5 |- T e. L
7		htthlem3.a	. . . . 5 |- ((x e. X /\ y e. X) -> ((T` x)Py) = (xP(T` y)))
8		htthlem3.f	. . . . 5 |- F = {<.m, w>. | (m e. NN /\ w = {<.v, u>. | (v e. X /\ u = ((T` v)P(f` m)))})}
9		htthlem3.c	. . . . 5 |- C = <.<. + , x. >., abs>.
10		htthlem3.d	. . . . 5 |- D = (U BLnOp C)
11		htthlem3.n	. . . . 5 |- N = (norm` U)
12		htthlem3.o	. . . . 5 |- O = (UnormOpC)
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	htthlem9 8624	. . . 4 |- ((f:NN-->X /\ k e. NN) -> ((N` (T` (f` k)))^2) = (abs` ((F` k)` (T` (f` k)))))
14	13	adantr 391	. . 3 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> ((N` (T` (f` k)))^2) = (abs` ((F` k)` (T` (f` k)))))
15	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	htthlem8 8623	. . . . 5 |- ((((F` k) e. D /\ d e. RR /\ (T` (f` k)) e. X) /\ (O` (F` k)) <_ d) -> (abs` ((F` k)` (T` (f` k)))) <_ (d x. (N` (T` (f` k)))))
16	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	htthlem5 8620	. . . . . . 7 |- ((f:NN-->X /\ k e. NN) -> (F` k) e. D)
17	16	adantr 391	. . . . . 6 |- (((f:NN-->X /\ k e. NN) /\ d e. RR) -> (F` k) e. D)
18		pm3.27 323	. . . . . 6 |- (((f:NN-->X /\ k e. NN) /\ d e. RR) -> d e. RR)
19	1, 3, 5, 6	htthlem1 8616	. . . . . . 7 |- ((f:NN-->X /\ k e. NN) -> (T` (f` k)) e. X)
20	19	adantr 391	. . . . . 6 |- (((f:NN-->X /\ k e. NN) /\ d e. RR) -> (T` (f` k)) e. X)
21	17, 18, 20	3jca 821	. . . . 5 |- (((f:NN-->X /\ k e. NN) /\ d e. RR) -> ((F` k) e. D /\ d e. RR /\ (T` (f` k)) e. X))
22	15, 21	sylan 450	. . . 4 |- ((((f:NN-->X /\ k e. NN) /\ d e. RR) /\ (O` (F` k)) <_ d) -> (abs` ((F` k)` (T` (f` k)))) <_ (d x. (N` (T` (f` k)))))
23	22	anasss 442	. . 3 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> (abs` ((F` k)` (T` (f` k)))) <_ (d x. (N` (T` (f` k)))))
24	14, 23	eqbrtrd 2640	. 2 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> ((N` (T` (f` k)))^2) <_ (d x. (N` (T` (f` k)))))
25		sqlecant 6642	. . 3 |- ((((N` (T` (f` k))) e. RR /\ 0 <_ (N` (T` (f` k)))) /\ (d e. RR /\ 0 <_ d)) -> (((N` (T` (f` k)))^2) <_ (d x. (N` (T` (f` k)))) <-> (N` (T` (f` k))) <_ d))
26	5	hlnvi 8592	. . . . . 6 |- U e. NrmCVec
27	1, 11	nvcl 8283	. . . . . 6 |- ((U e. NrmCVec /\ (T` (f` k)) e. X) -> (N` (T` (f` k))) e. RR)
28	26, 27	mpan 697	. . . . 5 |- ((T` (f` k)) e. X -> (N` (T` (f` k))) e. RR)
29	19, 28	syl 10	. . . 4 |- ((f:NN-->X /\ k e. NN) -> (N` (T` (f` k))) e. RR)
30	29	adantr 391	. . 3 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> (N` (T` (f` k))) e. RR)
31	1, 11	nvge0 8298	. . . . . 6 |- ((U e. NrmCVec /\ (T` (f` k)) e. X) -> 0 <_ (N` (T` (f` k))))
32	26, 31	mpan 697	. . . . 5 |- ((T` (f` k)) e. X -> 0 <_ (N` (T` (f` k))))
33	19, 32	syl 10	. . . 4 |- ((f:NN-->X /\ k e. NN) -> 0 <_ (N` (T` (f` k))))
34	33	adantr 391	. . 3 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> 0 <_ (N` (T` (f` k))))
35		simprl 416	. . 3 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> d e. RR)
36	9	cnnv 8303	. . . . . . . . . 10 |- C e. NrmCVec
37	9	cnnvba 8305	. . . . . . . . . . 11 |- CC = (Base` C)
38	1, 37, 10	blof 8441	. . . . . . . . . 10 |- ((U e. NrmCVec /\ C e. NrmCVec /\ (F` k) e. D) -> (F` k):X-->CC)
39	26, 36, 38	mp3an12 908	. . . . . . . . 9 |- ((F` k) e. D -> (F` k):X-->CC)
40	1, 37, 12	nmoge0 8426	. . . . . . . . . 10 |- ((U e. NrmCVec /\ C e. NrmCVec /\ (F` k):X-->CC) -> 0 <_ (O` (F` k)))
41	26, 36, 40	mp3an12 908	. . . . . . . . 9 |- ((F` k):X-->CC -> 0 <_ (O` (F` k)))
42	39, 41	syl 10	. . . . . . . 8 |- ((F` k) e. D -> 0 <_ (O` (F` k)))
43	42	adantr 391	. . . . . . 7 |- (((F` k) e. D /\ d e. RR) -> 0 <_ (O` (F` k)))
44		0re 5452	. . . . . . . . 9 |- 0 e. RR
45		letrt 5537	. . . . . . . . 9 |- ((0 e. RR /\ (O` (F` k)) e. RR /\ d e. RR) -> ((0 <_ (O` (F` k)) /\ (O` (F` k)) <_ d) -> 0 <_ d))
46	44, 45	mp3an1 905	. . . . . . . 8 |- (((O` (F` k)) e. RR /\ d e. RR) -> ((0 <_ (O` (F` k)) /\ (O` (F` k)) <_ d) -> 0 <_ d))
47	1, 37, 12, 10	nmblore 8442	. . . . . . . . 9 |- ((U e. NrmCVec /\ C e. NrmCVec /\ (F` k) e. D) -> (O` (F` k)) e. RR)
48	26, 36, 47	mp3an12 908	. . . . . . . 8 |- ((F` k) e. D -> (O` (F` k)) e. RR)
49	46, 48	sylan 450	. . . . . . 7 |- (((F` k) e. D /\ d e. RR) -> ((0 <_ (O` (F` k)) /\ (O` (F` k)) <_ d) -> 0 <_ d))
50	43, 49	mpand 703	. . . . . 6 |- (((F` k) e. D /\ d e. RR) -> ((O` (F` k)) <_ d -> 0 <_ d))
51	50	imp 350	. . . . 5 |- ((((F` k) e. D /\ d e. RR) /\ (O` (F` k)) <_ d) -> 0 <_ d)
52	51	anasss 442	. . . 4 |- (((F` k) e. D /\ (d e. RR /\ (O` (F` k)) <_ d)) -> 0 <_ d)
53	52, 16	sylan 450	. . 3 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> 0 <_ d)
54	25, 30, 34, 35, 53	syl2anc 474	. 2 |- (((f:NN-->X /\ k e. NN) /\ (d e. RR /\ (O` (F` k)) <_ d)) -> (((N` (T` (f` k)))^2) <_ (d x. (N` (T` (f` k)))) <-> (N` (T` (f` k))) <_ d))
55	24, 54