Theorem ubthlem10 8469

Description: Lemma for ubthi 8475. Upper limit for the norm of an operator value at auxiliary vector Q.

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
ubthlem10	|- (((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)) <_ 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 ubthlem10

Step	Hyp	Ref	Expression
1		ubthlem10.1	. . . . . . . 8 |- X = (Base` U)
2		ubthlem10.11	. . . . . . . 8 |- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
3	1, 2	ubthlem1 8460	. . . . . . 7 |- (k e. NN -> (Q e. (A` k) <-> (Q e. X /\ A.n e. NN (N` ((T` n)` Q)) <_ k)))
4	3	pm3.27bda 421	. . . . . 6 |- ((k e. NN /\ Q e. (A` k)) -> A.n e. NN (N` ((T` n)` Q)) <_ k)
5	4	ex 373	. . . . 5 |- (k e. NN -> (Q e. (A` k) -> A.n e. NN (N` ((T` n)` Q)) <_ k))
6		ra4 1686	. . . . 5 |- (A.n e. NN (N` ((T` n)` Q)) <_ k -> (n e. NN -> (N` ((T` n)` Q)) <_ k))
7	5, 6	syl6com 53	. . . 4 |- (Q e. (A` k) -> (k e. NN -> (n e. NN -> (N` ((T` n)` Q)) <_ k)))
8	7	com3l 34	. . 3 |- (k e. NN -> (n e. NN -> (Q e. (A` k) -> (N` ((T` n)` Q)) <_ k)))
9	8	imp31 362	. 2 |- (((k e. NN /\ n e. NN) /\ Q e. (A` k)) -> (N` ((T` n)` Q)) <_ k)
10		ssel 2053	. . . 4 |- ((p( ball ` D)r) (_ (A` k) -> (Q e. (p( ball ` D)r) -> Q e. (A` k)))
11	10	impcom 351	. . 3 |- ((Q e. (p( ball ` D)r) /\ (p( ball ` D)r) (_ (A` k)) -> Q e. (A` k))
12		ubthlem10.7	. . . . . . . . . . . . 13 |- U e. NrmCVec
13		ubthlem10.r	. . . . . . . . . . . . . 14 |- R = (.s` U)
14	1, 13	nvsass 8189	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ ((r / 2) e. CC /\ (1 / (L` x)) e. CC /\ x e. X)) -> (((r / 2) x. (1 / (L` x)))Rx) = ((r / 2)R((1 / (L` x))Rx)))
15	12, 14	mpan 693	. . . . . . . . . . . 12 |- (((r / 2) e. CC /\ (1 / (L` x)) e. CC /\ x e. X) -> (((r / 2) x. (1 / (L` x)))Rx) = ((r / 2)R((1 / (L` x))Rx)))
16		rehalfclt 5981	. . . . . . . . . . . . . 14 |- (r e. RR -> (r / 2) e. RR)
17	16	recnd 5287	. . . . . . . . . . . . 13 |- (r e. RR -> (r / 2) e. CC)
18	17	adantr 389	. . . . . . . . . . . 12 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> (r / 2) e. CC)
19		rerecclt 5759	. . . . . . . . . . . . . . 15 |- (((L` x) e. RR /\ (L` x) =/= 0) -> (1 / (L` x)) e. RR)
20		ubthlem10.n	. . . . . . . . . . . . . . . . . 18 |- L = (norm` U)
21	1, 20	nvcl 8227	. . . . . . . . . . . . . . . . 17 |- ((U e. NrmCVec /\ x e. X) -> (L` x) e. RR)
22	12, 21	mpan 693	. . . . . . . . . . . . . . . 16 |- (x e. X -> (L` x) e. RR)
23	22	adantr 389	. . . . . . . . . . . . . . 15 |- ((x e. X /\ x =/= Z) -> (L` x) e. RR)
24		ubthlem10.z	. . . . . . . . . . . . . . . . . . 19 |- Z = (0v` U)
25	1, 24, 20	nvz 8236	. . . . . . . . . . . . . . . . . 18 |- ((U e. NrmCVec /\ x e. X) -> ((L` x) = 0 <-> x = Z))
26	12, 25	mpan 693	. . . . . . . . . . . . . . . . 17 |- (x e. X -> ((L` x) = 0 <-> x = Z))
27	26	necon3bid 1593	. . . . . . . . . . . . . . . 16 |- (x e. X -> ((L` x) =/= 0 <-> x =/= Z))
28	27	biimpar 417	. . . . . . . . . . . . . . 15 |- ((x e. X /\ x =/= Z) -> (L` x) =/= 0)
29	19, 23, 28	sylanc 471	. . . . . . . . . . . . . 14 |- ((x e. X /\ x =/= Z) -> (1 / (L` x)) e. RR)
30	29	recnd 5287	. . . . . . . . . . . . 13 |- ((x e. X /\ x =/= Z) -> (1 / (L` x)) e. CC)
31	30	adantl 388	. . . . . . . . . . . 12 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> (1 / (L` x)) e. CC)
32		simprl 414	. . . . . . . . . . . 12 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> x e. X)
33	15, 18, 31, 32	syl3anc 856	. . . . . . . . . . 11 |- ((r e. RR /\ (x e. X /\ x =/= Z)) -> (((r / 2) x. (1 / (L` x)))Rx) = ((r / 2)R((1 / (L` x))Rx)))
34	33	adantlr 393	. . . . . . . . . 10 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (((r / 2) x. (1 / (L` x)))Rx) = ((r / 2)R((1 / (L` x))Rx)))
35	34	fveq2d 3713	. . . . . . . . 9 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (L` (((r / 2) x. (1 / (L` x)))Rx)) = (L` ((r / 2)R((1 / (L` x))Rx))))
36	1, 13, 20	nvsge0 8230	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ ((r / 2) e. RR /\ 0 <_ (r / 2)) /\ ((1 / (L` x))Rx) e. X) -> (L` ((r / 2)R((1 / (L` x))Rx))) = ((r / 2) x. (L` ((1 / (L` x))Rx))))
37	12, 36	mp3an1 900	. . . . . . . . . 10 |- ((((r / 2) e. RR /\ 0 <_ (r / 2)) /\ ((1 / (L` x))Rx) e. X) -> (L` ((r / 2)R((1 / (L` x))Rx))) = ((r / 2) x. (L` ((1 / (L` x))Rx))))
38	16	adantr 389	. . . . . . . . . . 11 |- ((r e. RR /\ 0 < r) -> (r / 2) e. RR)
39		halfpos2t 5984	. . . . . . . . . . . . 13 |- (r e. RR -> (0 < r <-> 0 < (r / 2)))
40	39	biimpa 416	. . . . . . . . . . . 12 |- ((r e. RR /\ 0 < r) -> 0 < (r / 2))
41		0re 5412	. . . . . . . . . . . . . . 15 |- 0 e. RR
42		ltlet 5493	. . . . . . . . . . . . . . 15 |- ((0 e. RR /\ (r / 2) e. RR) -> (0 < (r / 2) -> 0 <_ (r / 2)))
43	41, 42	mpan 693	. . . . . . . . . . . . . 14 |- ((r / 2) e. RR -> (0 < (r / 2) -> 0 <_ (r / 2)))
44	16, 43	syl 10	. . . . . . . . . . . . 13 |- (r e. RR -> (0 < (r / 2) -> 0 <_ (r / 2)))
45	44	adantr 389	. . . . . . . . . . . 12 |- ((r e. RR /\ 0 < r) -> (0 < (r / 2) -> 0 <_ (r / 2)))
46	40, 45	mpd 26	. . . . . . . . . . 11 |- ((r e. RR /\ 0 < r) -> 0 <_ (r / 2))
47	38, 46	jca 288	. . . . . . . . . 10 |- ((r e. RR /\ 0 < r) -> ((r / 2) e. RR /\ 0 <_ (r / 2)))
48	1, 13	nvscl 8187	. . . . . . . . . . . 12 |- ((U e. NrmCVec /\ (1 / (L` x)) e. CC /\ x e. X) -> ((1 / (L` x))Rx) e. X)
49	12, 48	mp3an1 900	. . . . . . . . . . 11 |- (((1 / (L` x)) e. CC /\ x e. X) -> ((1 / (L` x))Rx) e. X)
50		pm3.26 319	. . . . . . . . . . 11 |- ((x e. X /\ x =/= Z) -> x e. X)
51	49, 30, 50	sylanc 471	. . . . . . . . . 10 |- ((x e. X /\ x =/= Z) -> ((1 / (L` x))Rx) e. X)
52	37, 47, 51	syl2an 454	. . . . . . . . 9 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (L` ((r / 2)R((1 / (L` x))Rx))) = ((r / 2) x. (L` ((1 / (L` x))Rx))))
53	35, 52	eqtrd 1499	. . . . . . . 8 |- (((r e. RR /\ 0 < r) /\ (x e. X /\ x =/= Z)) -> (L` (((r /