Theorem ubthlem12 8540

Description: Lemma for ubthi 8544. Upper limit for the norm of an operator value at x.

Hypotheses

Ref	Expression
ubthlem10.1	|- X = (Base` U)
ubthlem10.2	|- Y = (Base` W)
ubthlem10.3	|- N = (norm` W)
ubthlem10.4	|- O = (UnormOpW)
ubthlem10.5	|- B = (U BLnOp W)
ubthlem10.6	|- T:NN-->B
ubthlem10.7	|- U e. NrmCVec
ubthlem10.8	|- W e. NrmCVec
ubthlem10.9	|- D = (IndMet` U)
ubthlem10.n	|- L = (norm` U)
ubthlem10.g	|- G = (+v` U)
ubthlem10.m	|- M = (-v` U)
ubthlem10.r	|- R = (.s` U)
ubthlem10.z	|- Z = (0v` U)
ubthlem10.11	|- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
ubthlem10.q	|- Q = (pG(((r / 2) x. (1 / (L` x)))Rx))

Assertion

Ref	Expression
ubthlem12	|- (((k e. NN /\ n e. NN) /\ ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) /\ (p( ball ` D)r) (_ (A` k))) -> (N` ((T` n)` x)) <_ (((2 / r) x. (2 x. k)) x. (L` x)))

Distinct variable groups:   k,n,p,r,x,A   D,k,n,p,r,x   x,L   h,j,k,n,x,y,z,N   k,O,p,r   Q,h,n,z   h,p,r,T,j,k,n,y,z,x   x,U   x,W   j,X,k,n,r,x,y,z

Proof of Theorem ubthlem12

Step	Hyp	Ref	Expression
1		lemul2it 5839	. . 3 |- ((((N` ((T` n)` (QMp))) e. RR /\ (2 x. k) e. RR /\ (((2 / r) x. (L` x)) e. RR /\ 0 <_ ((2 / r) x. (L` x)))) /\ (N` ((T` n)` (QMp))) <_ (2 x. k)) -> (((2 / r) x. (L` x)) x. (N` ((T` n)` (QMp)))) <_ (((2 / r) x. (L` x)) x. (2 x. k)))
2		ffvelrn 3814	. . . . . . . 8 |- (((T` n):X-->Y /\ (QMp) e. X) -> ((T` n)` (QMp)) e. Y)
3		ubthlem10.6	. . . . . . . . . 10 |- T:NN-->B
4	3	ffvelrni 3815	. . . . . . . . 9 |- (n e. NN -> (T` n) e. B)
5		ubthlem10.7	. . . . . . . . . 10 |- U e. NrmCVec
6		ubthlem10.8	. . . . . . . . . 10 |- W e. NrmCVec
7		ubthlem10.1	. . . . . . . . . . 11 |- X = (Base` U)
8		ubthlem10.2	. . . . . . . . . . 11 |- Y = (Base` W)
9		ubthlem10.5	. . . . . . . . . . 11 |- B = (U BLnOp W)
10	7, 8, 9	blof 8445	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ (T` n) e. B) -> (T` n):X-->Y)
11	5, 6, 10	mp3an12 906	. . . . . . . . 9 |- ((T` n) e. B -> (T` n):X-->Y)
12	4, 11	syl 10	. . . . . . . 8 |- (n e. NN -> (T` n):X-->Y)
13		ubthlem10.n	. . . . . . . . . . 11 |- L = (norm` U)
14		ubthlem10.g	. . . . . . . . . . 11 |- G = (+v` U)
15		ubthlem10.m	. . . . . . . . . . 11 |- M = (-v` U)
16		ubthlem10.r	. . . . . . . . . . 11 |- R = (.s` U)
17		ubthlem10.z	. . . . . . . . . . 11 |- Z = (0v` U)
18		ubthlem10.q	. . . . . . . . . . 11 |- Q = (pG(((r / 2) x. (1 / (L` x)))Rx))
19	7, 5, 13, 14, 15, 16, 17, 18	ubthlem7 8535	. . . . . . . . . 10 |- ((p e. X /\ (r e. RR /\ (x e. X /\ x =/= Z))) -> Q e. X)
20	19	adantrlr 401	. . . . . . . . 9 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> Q e. X)
21	7, 15	nvmcl 8267	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ Q e. X /\ p e. X) -> (QMp) e. X)
22	5, 21	mp3an1 903	. . . . . . . . . 10 |- ((Q e. X /\ p e. X) -> (QMp) e. X)
23	22	ancoms 436	. . . . . . . . 9 |- ((p e. X /\ Q e. X) -> (QMp) e. X)
24	20, 23	syldan 467	. . . . . . . 8 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> (QMp) e. X)
25	2, 12, 24	syl2an 454	. . . . . . 7 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> ((T` n)` (QMp)) e. Y)
26		ubthlem10.3	. . . . . . . . 9 |- N = (norm` W)
27	8, 26	nvcl 8287	. . . . . . . 8 |- ((W e. NrmCVec /\ ((T` n)` (QMp)) e. Y) -> (N` ((T` n)` (QMp))) e. RR)
28	6, 27	mpan 695	. . . . . . 7 |- (((T` n)` (QMp)) e. Y -> (N` ((T` n)` (QMp))) e. RR)
29	25, 28	syl 10	. . . . . 6 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (N` ((T` n)` (QMp))) e. RR)
30	29	adantll 392	. . . . 5 |- (((k e. NN /\ n e. NN) /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (N` ((T` n)` (QMp))) e. RR)
31		nnret 5929	. . . . . . 7 |- (k e. NN -> k e. RR)
32		2re 5979	. . . . . . . 8 |- 2 e. RR
33		axmulrcl 5274	. . . . . . . 8 |- ((2 e. RR /\ k e. RR) -> (2 x. k) e. RR)
34	32, 33	mpan 695	. . . . . . 7 |- (k e. RR -> (2 x. k) e. RR)
35	31, 34	syl 10	. . . . . 6 |- (k e. NN -> (2 x. k) e. RR)
36	35	ad2antrr 404	. . . . 5 |- (((k e. NN /\ n e. NN) /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (2 x. k) e. RR)
37		axmulrcl 5274	. . . . . . . . 9 |- (((2 / r) e. RR /\ (L` x) e. RR) -> ((2 / r) x. (L` x)) e. RR)
38		gt0ne0t 5618	. . . . . . . . . 10 |- ((r e. RR /\ 0 < r) -> r =/= 0)
39		redivclt 5800	. . . . . . . . . . 11 |- ((2 e. RR /\ r e. RR /\ r =/= 0) -> (2 / r) e. RR)
40	32, 39	mp3an1 903	. . . . . . . . . 10 |- ((r e. RR /\ r =/= 0) -> (2 / r) e. RR)
41	38, 40	syldan 467	. . . . . . . . 9 |- ((r e. RR /\ 0 < r) -> (2 / r) e. RR)
42	7, 13	nvcl 8287	. . . . . . . . . 10 |- ((U e. NrmCVec /\ x e. X) -> (L` x) e. RR)
43	5, 42	mpan 695	. . . . . . . . 9 |- (x e. X -> (L` x) e. RR)
44	37, 41, 43	syl2an 454	. . . . . . . 8 |- (((r e. RR /\ 0 < r) /\ x e. X) -> ((2 / r) x. (L` x)) e. RR)
45		mulge0t 5679	. . . . . . . . . 10 |- ((((2 / r) e. RR /\ (L` x) e. RR) /\ (0 <_ (2 / r) /\ 0 <_ (L` x))) -> 0 <_ ((2 / r) x. (L` x)))
46	45	an4s 508	. . . . . . . . 9 |- ((((2 / r) e. RR /\ 0 <_ (2 / r)) /\ ((L` x) e. RR /\ 0 <_ (L` x))) -> 0 <_ ((2 / r) x. (L` x)))
47		0re 5440	. . . . . . . . . . . 12 |- 0 e. RR
48		2pos 5989	. . . . . . . . . . . 12 |- 0 < 2
49	47, 32, 48	ltlei 5581	. . . . . . . . . . 11 |- 0 <_ 2
50		divge0t 5856	. . . . . . . . . . 11 |- (((2 e. RR /\ 0 <_ 2) /\ (r e. RR /\ 0 < r)) -> 0 <_ (2 / r))
51	32, 49, 50	mpanl12 708	. . . . . . . . . 10 |- ((r e. RR /\ 0 < r) -> 0 <_ (2 / r))
52	41, 51	jca 288	. . . . . . . . 9 |- ((r e. RR /\ 0 < r) -> ((2 / r) e. RR /\ 0 <_ (2 / r)))
53	7, 13	nvge0 8302	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ x e. X) -> 0 <_ (L` x))
54	5, 53	mpan 695	. . . . . . . . . 10 |- (x e. X -> 0 <_ (L` x))
55	43, 54	jca 288	. . . . . . . . 9 |- (x e. X -> ((L` x) e. RR /\ 0 <_ (L` x)))
56	46, 52, 55	syl2an 454	. . . . . . . 8 |- (((r e. RR /\ 0 < r) /\ x e. X) -> 0 <_ ((2 / r) x. (L` x)))
57	44, 56	jca 288	. . . . . . 7 |- (((r e. RR /\ 0 < r) /\ x e. X) -> (((2 / r) x. (L` x)) e. RR /\ 0 <_ ((2 / r) x. (L` x))))
58	57	adantrr 395	. . . . . 6 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (((2 / r) x. (L` x)) e. RR /\ 0 <_ ((2 / r) x. (L` x))))
59	58	ad2antll 407	. . . . 5 |- (((k e. NN /\ n e. NN) /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (((2 / r) x. (L` x)) e. RR /\ 0 <_ ((2 / r) x. (L` x))))
60	30, 36, 59	3jca 819	. . . 4 |- (((k e. NN /\ n e. NN) /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> ((N` ((T` n)` (QMp))) e. RR /\ (2 x. k) e. RR /\ (((2 / r) x. (L` x)) e. RR /\ 0 <_ ((2 / r) x. (L` x)))))
61	60	adantrr 395	. . 3 |- (((k e. NN /\ n e. NN) /\ ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e.