Theorem blocnilem 8395

Description: Lemma for blocni 8396 and lnocni 8397. If a linear operator is continuous at any point, it is bounded. Warning: The HTML proof page is 0.7MB in size.

Hypotheses

Ref	Expression
blocni.8	|- C = (IndMet` U)
blocni.d	|- D = (IndMet` W)
blocni.j	|- J = (Open` C)
blocni.k	|- K = (Open` D)
blocni.4	|- L = (U LnOp W)
blocni.5	|- B = (U BLnOp W)
blocni.u	|- U e. NrmCVec
blocni.w	|- W e. NrmCVec
blocni.l	|- T e. L
blocnilem.1	|- X = (Base` U)

Assertion

Ref	Expression
blocnilem	|- ((P e. X /\ T e. ((J CnP K)` P)) -> T e. B)

Proof of Theorem blocnilem

Step	Hyp	Ref	Expression
1		blocni.w	. . . . 5 |- W e. NrmCVec
2		blocni.u	. . . . . 6 |- U e. NrmCVec
3		1re 5407	. . . . . . 7 |- 1 e. RR
4		lt01 5653	. . . . . . . 8 |- 0 < 1
5		blocnilem.1	. . . . . . . . 9 |- X = (Base` U)
6		eqid 1468	. . . . . . . . 9 |- (norm` U) = (norm` U)
7		eqid 1468	. . . . . . . . 9 |- (norm` W) = (norm` W)
8		eqid 1468	. . . . . . . . 9 |- (-v` U) = (-v` U)
9		blocni.8	. . . . . . . . 9 |- C = (IndMet` U)
10		blocni.d	. . . . . . . . 9 |- D = (IndMet` W)
11		blocni.j	. . . . . . . . 9 |- J = (Open` C)
12		blocni.k	. . . . . . . . 9 |- K = (Open` D)
13		blocni.4	. . . . . . . . 9 |- L = (U LnOp W)
14		blocni.l	. . . . . . . . 9 |- T e. L
15	5, 6, 7, 8, 9, 10, 11, 12, 13, 14	nvcnpi4 8355	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ 1 e. RR /\ 0 < 1)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
16	4, 15	mp3anr3 912	. . . . . . 7 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ (T e. ((J CnP K)` P) /\ 1 e. RR)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
17	3, 16	mpanr2 708	. . . . . 6 |- (((U e. NrmCVec /\ W e. NrmCVec /\ P e. X) /\ T e. ((J CnP K)` P)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
18	2, 17	mp3anl1 907	. . . . 5 |- (((W e. NrmCVec /\ P e. X) /\ T e. ((J CnP K)` P)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
19	1, 18	mpanl1 704	. . . 4 |- ((P e. X /\ T e. ((J CnP K)` P)) -> E.z e. RR (0 < z /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)))
20		opreq1 3953	. . . . . . . . . . . 12 |- (x = (1 / z) -> (x x. ((norm` U)` w)) = ((1 / z) x. ((norm` U)` w)))
21	20	breq2d 2620	. . . . . . . . . . 11 |- (x = (1 / z) -> (((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)) <-> ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
22	21	ralbidv 1655	. . . . . . . . . 10 |- (x = (1 / z) -> (A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)) <-> A.w e. X ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))))
23	22	rcla4ev 1868	. . . . . . . . 9 |- (((1 / z) e. RR /\ A.w e. X ((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w))) -> E.x e. RR A.w e. X ((norm` W)` (T` w)) <_ (x x. ((norm` U)` w)))
24		gt0ne0t 5592	. . . . . . . . . . 11 |- ((z e. RR /\ 0 < z) -> z =/= 0)
25		rerecclt 5759	. . . . . . . . . . 11 |- ((z e. RR /\ z =/= 0) -> (1 / z) e. RR)
26	24, 25	syldan 467	. . . . . . . . . 10 |- ((z e. RR /\ 0 < z) -> (1 / z) e. RR)
27	26	ad2antlr 405	. . . . . . . . 9 |- (((P e. X /\ (z e. RR /\ 0 < z)) /\ A.y e. X (((norm` U)` (P(-v` U)y)) <_ z -> ((norm` W)` (T` (P(-v` U)y))) <_ 1)) -> (1 / z) e. RR)
28		fveq2 3709	. . . . . . . . . . . . 13 |- (w = (0v` U) -> (T` w) = (T` (0v` U)))
29	28	fveq2d 3713	. . . . . . . . . . . 12 |- (w = (0v` U) -> ((norm` W)` (T` w)) = ((norm` W)` (T` (0v` U))))
30		fveq2 3709	. . . . . . . . . . . . 13 |- (w = (0v` U) -> ((norm` U)` w) = ((norm` U)` (0v` U)))
31	30	opreq2d 3961	. . . . . . . . . . . 12 |- (w = (0v` U) -> ((1 / z) x. ((norm` U)` w)) = ((1 / z) x. ((norm` U)` (0v` U))))
32	29, 31	breq12d 2621	. . . . . . . . . . 11 |- (w = (0v` U) -> (((norm` W)` (T` w)) <_ ((1 / z) x. ((norm` U)` w)) <-> ((norm` W)` (T` (0v` U))) <_ ((1 / z) x. ((norm` U)` (0v` U)))))
33	5, 8	nvnncan 8223	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((U e. NrmCVec /\ P e. X /\ ((z / ((norm` U)` w))(.s` U)w) e. X) -> (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))) = ((z / ((norm` U)` w))(.s` U)w))
34	2, 33	mp3an1 900	. . . . . . . . . . . . . . . . . . . . . 22 |- ((P e. X /\ ((z / ((norm` U)` w))(.s` U)w) e. X) -> (P(-v` U)(P(-v` U)((z / ((norm` U)` w))(.s` U)w))) = ((z / ((norm` U)` w))(.s` U)w))
35		simpll 412	. . . . . . . . . . . . . . . . . . . . . 22 |- (((P e. X /\ z e. RR) /\ (w e. X /\ w =/= (0v` U))) -> P e. X)
36		eqid 1468	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (.s` U) = (.s` U)
37	5, 36	nvscl 8187	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((U e. NrmCVec /\ (z / ((norm` U)` w)) e. CC /\ w e. X) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
38	2, 37	mp3an1 900	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((z / ((norm` U)` w)) e. CC /\ w e. X) -> ((z / ((norm` U)` w))(.s` U)w) e. X)
39		redivclt 5756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((z e. RR /\ ((norm` U)` w) e. RR /\ ((norm` U)` w) =/= 0) -> (z / ((norm` U)` w)) e. RR)
40	39	3expb 832	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((z e. RR /\ (((norm` U)` w) e. RR /\ ((norm` U)` w) =/= 0)) -> (z / ((norm` U)` w)) e. RR)
41	5, 6	nvcl 8227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((U e. NrmCVec /\ w e. X) -> ((norm` U)` w) e. RR)
42	2, 41	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. X -> ((norm` U)` w) e. RR)
43	42	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. X /\ w =/= (0v` U)) -> ((norm` U)` w) e. RR)
44		eqid 1468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (0v` U) = (0v` U)
45	5, 44, 6	nvz 8236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((U e. NrmCVec /\ w e. X) -> (((norm` U)` w) = 0 <-> w = (0v` U)))
46	2, 45	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w e. X -> (((norm` U)` w) = 0 <-> w = (0v` U)))
47	46	necon3bid 1593	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (w e. X -> (((norm` U)` w) =/= 0 <-> w =/= (0v` U)))
48	47	biimpar 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w e. X /\ w =/= (0v` U)) -> ((norm` U)` w) =/= 0)
49	43, 48	jca 288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. X /\ w =/= (0v` U)) -> (((norm` U)` w) e. RR /\ ((norm` U)` w) =/= 0))
50	40, 49	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. RR)
51	50	recnd 5287	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> (z / ((norm` U)` w)) e. CC)
52		simprl 414	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. RR /\ (w e. X /\ w =/= (0v` U))) -> w e. X)
53	38, 51, 52