Theorem ubthlem13 8485

Description: Lemma for ubthi 8488. Upper bound for the operator norm of any operator T` n.

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
ubthlem13	|- (((k e. NN /\ n e. NN) /\ ((p e. X /\ (r e. RR /\ 0 < r)) /\ (p( ball ` D)r) (_ (A` k))) -> (O` (T` n)) <_ ((2 / r) x. (2 x. k)))

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 ubthlem13

Step	Hyp	Ref	Expression
1		ubthlem10.1	. . 3 |- X = (Base` U)
2		ubthlem10.z	. . 3 |- Z = (0v` U)
3		ubthlem10.n	. . 3 |- L = (norm` U)
4		ubthlem10.3	. . 3 |- N = (norm` W)
5		ubthlem10.4	. . 3 |- O = (UnormOpW)
6		eqid 1473	. . 3 |- (U LnOp W) = (U LnOp W)
7		ubthlem10.7	. . 3 |- U e. NrmCVec
8		ubthlem10.8	. . 3 |- W e. NrmCVec
9	1, 2, 3, 4, 5, 6, 7, 8	nmlnoubi 8401	. 2 |- (((T` n) e. (U LnOp W) /\ (((2 / r) x. (2 x. k)) e. RR /\ 0 <_ ((2 / r) x. (2 x. k))) /\ A.x e. X (x =/= Z -> (N` ((T` n)` x)) <_ (((2 / r) x. (2 x. k)) x. (L` x)))) -> (O` (T` n)) <_ ((2 / r) x. (2 x. k)))
10		ubthlem10.6	. . . . 5 |- T:NN-->B
11	10	ffvelrni 3806	. . . 4 |- (n e. NN -> (T` n) e. B)
12		ubthlem10.5	. . . . . 6 |- B = (U BLnOp W)
13	6, 12	bloln 8389	. . . . 5 |- ((U e. NrmCVec /\ W e. NrmCVec /\ (T` n) e. B) -> (T` n) e. (U LnOp W))
14	7, 8, 13	mp3an12 904	. . . 4 |- ((T` n) e. B -> (T` n) e. (U LnOp W))
15	11, 14	syl 10	. . 3 |- (n e. NN -> (T` n) e. (U LnOp W))
16	15	ad2antlr 405	. 2 |- (((k e. NN /\ n e. NN) /\ ((p e. X /\ (r e. RR /\ 0 < r)) /\ (p( ball ` D)r) (_ (A` k))) -> (T` n) e. (U LnOp W))
17		axmulrcl 5254	. . . . . . 7 |- (((2 / r) e. RR /\ (2 x. k) e. RR) -> ((2 / r) x. (2 x. k)) e. RR)
18		gt0ne0t 5600	. . . . . . . 8 |- ((r e. RR /\ 0 < r) -> r =/= 0)
19		2re 5934	. . . . . . . . 9 |- 2 e. RR
20		redivclt 5764	. . . . . . . . 9 |- ((2 e. RR /\ r e. RR /\ r =/= 0) -> (2 / r) e. RR)
21	19, 20	mp3an1 901	. . . . . . . 8 |- ((r e. RR /\ r =/= 0) -> (2 / r) e. RR)
22	18, 21	syldan 467	. . . . . . 7 |- ((r e. RR /\ 0 < r) -> (2 / r) e. RR)
23		nnret 5885	. . . . . . . 8 |- (k e. NN -> k e. RR)
24		axmulrcl 5254	. . . . . . . . 9 |- ((2 e. RR /\ k e. RR) -> (2 x. k) e. RR)
25	19, 24	mpan 694	. . . . . . . 8 |- (k e. RR -> (2 x. k) e. RR)
26	23, 25	syl 10	. . . . . . 7 |- (k e. NN -> (2 x. k) e. RR)
27	17, 22, 26	syl2an 454	. . . . . 6 |- (((r e. RR /\ 0 < r) /\ k e. NN) -> ((2 / r) x. (2 x. k)) e. RR)
28		mulge0t 5660	. . . . . . . 8 |- ((((2 / r) e. RR /\ (2 x. k) e. RR) /\ (0 <_ (2 / r) /\ 0 <_ (2 x. k))) -> 0 <_ ((2 / r) x. (2 x. k)))
29	28	an4s 508	. . . . . . 7 |- ((((2 / r) e. RR /\ 0 <_ (2 / r)) /\ ((2 x. k) e. RR /\ 0 <_ (2 x. k))) -> 0 <_ ((2 / r) x. (2 x. k)))
30		0re 5420	. . . . . . . . . 10 |- 0 e. RR
31		2pos 5944	. . . . . . . . . 10 |- 0 < 2
32	30, 19, 31	ltlei 5562	. . . . . . . . 9 |- 0 <_ 2
33		divge0t 5818	. . . . . . . . 9 |- (((2 e. RR /\ 0 <_ 2) /\ (r e. RR /\ 0 < r)) -> 0 <_ (2 / r))
34	19, 32, 33	mpanl12 707	. . . . . . . 8 |- ((r e. RR /\ 0 < r) -> 0 <_ (2 / r))
35	22, 34	jca 288	. . . . . . 7 |- ((r e. RR /\ 0 < r) -> ((2 / r) e. RR /\ 0 <_ (2 / r)))
36		mulge0t 5660	. . . . . . . . . . 11 |- (((2 e. RR /\ k e. RR) /\ (0 <_ 2 /\ 0 <_ k)) -> 0 <_ (2 x. k))
37	36	an4s 508	. . . . . . . . . 10 |- (((2 e. RR /\ 0 <_ 2) /\ (k e. RR /\ 0 <_ k)) -> 0 <_ (2 x. k))
38	19, 32, 37	mpanl12 707	. . . . . . . . 9 |- ((k e. RR /\ 0 <_ k) -> 0 <_ (2 x. k))
39		ltlet 5501	. . . . . . . . . . 11 |- ((0 e. RR /\ k e. RR) -> (0 < k -> 0 <_ k))
40	30, 39	mpan 694	. . . . . . . . . 10 |- (k e. RR -> (0 < k -> 0 <_ k))
41		nngt0t 5902	. . . . . . . . . 10 |- (k e. NN -> 0 < k)
42	40, 23, 41	sylc 68	. . . . . . . . 9 |- (k e. NN -> 0 <_ k)
43	38, 23, 42	sylanc 471	. . . . . . . 8 |- (k e. NN -> 0 <_ (2 x. k))
44	26, 43	jca 288	. . . . . . 7 |- (k e. NN -> ((2 x. k) e. RR /\ 0 <_ (2 x. k)))
45	29, 35, 44	syl2an 454	. . . . . 6 |- (((r e. RR /\ 0 < r) /\ k e. NN) -> 0 <_ ((2 / r) x. (2 x. k)))
46	27, 45	jca 288	. . . . 5 |- (((r e. RR /\ 0 < r) /\ k e. NN) -> (((2 / r) x. (2 x. k)) e. RR /\ 0 <_ ((2 / r) x. (2 x. k))))
47	46	ancoms 436	. . . 4 |- ((k e. NN /\ (r e. RR /\ 0 < r)) -> (((2 / r) x. (2 x. k)) e. RR /\ 0 <_ ((2 / r) x. (2 x. k))))
48	47	adantrl 394	. . 3 |- ((k e. NN /\ (p e. X /\ (r e. RR /\ 0 < r))) -> (((2 / r) x. (2 x. k)) e. RR /\ 0 <_ ((2 / r) x. (2 x. k))))
49	48	ad2ant2r 409	. 2 |- (((k e. NN /\ n e. NN) /\ ((p e. X /\ (r e. RR /\ 0 < r)) /\ (p( ball ` D)r) (_ (A` k))) -> (((2 / r) x. (2 x. k)) e. RR /\ 0 <_ ((2 / r) x. (2 x. k))))
50		ubthlem10.2	. . . . . . . . . 10 |- Y = (Base` W)
51		ubthlem10.9	. . . . . . . . . 10 |- D = (IndMet` U)
52		ubthlem10.g	. . . . . . . . . 10 |- G = (+v` U)
53		ubthlem10.m	. . . . . . . . . 10 |- M = (-v` U)
54		ubthlem10.r	. . . . . . . . . 10 |- R = (.s` U)
55		ubthlem10.11	. . . . . . . . . 10 |- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
56		ubthlem10.q	. . . . . . . . . 10 |- Q = (pG(((r / 2) x. (1 / (L` x)))Rx))
57	1, 50, 4, 5, 12, 10, 7, 8, 51, 3, 52, 53, 54, 2, 55, 56	ubthlem12 8484	. . . . . . . . 9 |- (((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)))
58	57	exp32 377	. . . . . . . 8 |- ((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)))))
59	58	exp4d 381	. . . . . . 7 |- ((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)))))))
60	59	imp3a 361	. . . . . 6 |- ((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))))))
61	60	com34 36	. . . . 5 |- ((k e. NN /\ n e. NN) -> ((p e. X /\ (r e. RR /\ 0 < r)) -> ((p( ball ` D)r) (_ (A` k) -> ((x e. X /\ x