Theorem ubthlem11 8535

Description: Lemma for ubthi 8540. Upper limit for the norm of an operator value at Q - p.

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
ubthlem11	|- (((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)` (QMp))) <_ (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 ubthlem11

Step	Hyp	Ref	Expression
1		ubthlem10.8	. . . . . . 7 |- W e. NrmCVec
2		ubthlem10.2	. . . . . . . 8 |- Y = (Base` W)
3		eqid 1478	. . . . . . . 8 |- (-v` W) = (-v` W)
4	2, 3	nvmcl 8263	. . . . . . 7 |- ((W e. NrmCVec /\ ((T` n)` Q) e. Y /\ ((T` n)` p) e. Y) -> (((T` n)` Q)(-v` W)((T` n)` p)) e. Y)
5	1, 4	mp3an1 905	. . . . . 6 |- ((((T` n)` Q) e. Y /\ ((T` n)` p) e. Y) -> (((T` n)` Q)(-v` W)((T` n)` p)) e. Y)
6		ffvelrn 3820	. . . . . . 7 |- (((T` n):X-->Y /\ Q e. X) -> ((T` n)` Q) e. Y)
7		ubthlem10.6	. . . . . . . . 9 |- T:NN-->B
8	7	ffvelrni 3821	. . . . . . . 8 |- (n e. NN -> (T` n) e. B)
9		ubthlem10.7	. . . . . . . . 9 |- U e. NrmCVec
10		ubthlem10.1	. . . . . . . . . 10 |- X = (Base` U)
11		ubthlem10.5	. . . . . . . . . 10 |- B = (U BLnOp W)
12	10, 2, 11	blof 8441	. . . . . . . . 9 |- ((U e. NrmCVec /\ W e. NrmCVec /\ (T` n) e. B) -> (T` n):X-->Y)
13	9, 1, 12	mp3an12 908	. . . . . . . 8 |- ((T` n) e. B -> (T` n):X-->Y)
14	8, 13	syl 10	. . . . . . 7 |- (n e. NN -> (T` n):X-->Y)
15		ubthlem10.n	. . . . . . . . 9 |- L = (norm` U)
16		ubthlem10.g	. . . . . . . . 9 |- G = (+v` U)
17		ubthlem10.m	. . . . . . . . 9 |- M = (-v` U)
18		ubthlem10.r	. . . . . . . . 9 |- R = (.s` U)
19		ubthlem10.z	. . . . . . . . 9 |- Z = (0v` U)
20		ubthlem10.q	. . . . . . . . 9 |- Q = (pG(((r / 2) x. (1 / (L` x)))Rx))
21	10, 9, 15, 16, 17, 18, 19, 20	ubthlem7 8531	. . . . . . . 8 |- ((p e. X /\ (r e. RR /\ (x e. X /\ x =/= Z))) -> Q e. X)
22	21	adantrlr 403	. . . . . . 7 |- ((p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z))) -> Q e. X)
23	6, 14, 22	syl2an 456	. . . . . 6 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> ((T` n)` Q) e. Y)
24		ffvelrn 3820	. . . . . . . 8 |- (((T` n):X-->Y /\ p e. X) -> ((T` n)` p) e. Y)
25	24, 14	sylan 450	. . . . . . 7 |- ((n e. NN /\ p e. X) -> ((T` n)` p) e. Y)
26	25	adantrr 397	. . . . . 6 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> ((T` n)` p) e. Y)
27	5, 23, 26	sylanc 473	. . . . 5 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (((T` n)` Q)(-v` W)((T` n)` p)) e. Y)
28		ubthlem10.3	. . . . . . 7 |- N = (norm` W)
29	2, 28	nvcl 8283	. . . . . 6 |- ((W e. NrmCVec /\ (((T` n)` Q)(-v` W)((T` n)` p)) e. Y) -> (N` (((T` n)` Q)(-v` W)((T` n)` p))) e. RR)
30	1, 29	mpan 697	. . . . 5 |- ((((T` n)` Q)(-v` W)((T` n)` p)) e. Y -> (N` (((T` n)` Q)(-v` W)((T` n)` p))) e. RR)
31	27, 30	syl 10	. . . 4 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (N` (((T` n)` Q)(-v` W)((T` n)` p))) e. RR)
32	31	ad2ant2lr 412	. . 3 |- (((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)` Q)(-v` W)((T` n)` p))) e. RR)
33		axaddrcl 5284	. . . . 5 |- (((N` ((T` n)` Q)) e. RR /\ (N` ((T` n)` p)) e. RR) -> ((N` ((T` n)` Q)) + (N` ((T` n)` p))) e. RR)
34	2, 28	nvcl 8283	. . . . . . 7 |- ((W e. NrmCVec /\ ((T` n)` Q) e. Y) -> (N` ((T` n)` Q)) e. RR)
35	1, 34	mpan 697	. . . . . 6 |- (((T` n)` Q) e. Y -> (N` ((T` n)` Q)) e. RR)
36	23, 35	syl 10	. . . . 5 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (N` ((T` n)` Q)) e. RR)
37	2, 28	nvcl 8283	. . . . . . . 8 |- ((W e. NrmCVec /\ ((T` n)` p) e. Y) -> (N` ((T` n)` p)) e. RR)
38	1, 37	mpan 697	. . . . . . 7 |- (((T` n)` p) e. Y -> (N` ((T` n)` p)) e. RR)
39	25, 38	syl 10	. . . . . 6 |- ((n e. NN /\ p e. X) -> (N` ((T` n)` p)) e. RR)
40	39	adantrr 397	. . . . 5 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (N` ((T` n)` p)) e. RR)
41	33, 36, 40	sylanc 473	. . . 4 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> ((N` ((T` n)` Q)) + (N` ((T` n)` p))) e. RR)
42	41	ad2ant2lr 412	. . 3 |- (((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)` Q)) + (N` ((T` n)` p))) e. RR)
43		axaddrcl 5284	. . . . 5 |- ((k e. RR /\ k e. RR) -> (k + k) e. RR)
44		nnret 5931	. . . . 5 |- (k e. NN -> k e. RR)
45	43, 44, 44	sylanc 473	. . . 4 |- (k e. NN -> (k + k) e. RR)
46	45	ad2antrr 406	. . 3 |- (((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))) -> (k + k) e. RR)
47	2, 3, 28	nvmtri 8295	. . . . . 6 |- ((W e. NrmCVec /\ ((T` n)` Q) e. Y /\ ((T` n)` p) e. Y) -> (N` (((T` n)` Q)(-v` W)((T` n)` p))) <_ ((N` ((T` n)` Q)) + (N` ((T` n)` p))))
48	1, 47	mp3an1 905	. . . . 5 |- ((((T` n)` Q) e. Y /\ ((T` n)` p) e. Y) -> (N` (((T` n)` Q)(-v` W)((T` n)` p))) <_ ((N` ((T` n)` Q)) + (N` ((T` n)` p))))
49	48, 23, 26	sylanc 473	. . . 4 |- ((n e. NN /\ (p e. X /\ ((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)))) -> (N` (((T` n)` Q)(-v` W)((T` n)` p))) <_ ((N` ((T` n)` Q)) +