Theorem ubthlem3 8531

Description: Lemma for ubthi 8544. The limit of any sequence in A` k has operator value norm less than k, for any bounded linear operator T` n, using metcn4i 7972 (with continuity shown by blocn2 8468) and the properties of A` k.

Hypotheses

Ref	Expression
ubthlem3.1	|- X = (Base` U)
ubthlem3.2	|- Y = (Base` W)
ubthlem3.3	|- N = (norm` W)
ubthlem3.5	|- B = (U BLnOp W)
ubthlem3.6	|- T:NN-->B
ubthlem3.u	|- U e. NrmCVec
ubthlem3.w	|- W e. NrmCVec
ubthlem3.9c	|- C = (IndMet` U)
ubthlem3.9d	|- D = (IndMet` W)
ubthlem3.11	|- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
ubthlem3.12	|- G = {<.m, x>. | (m e. NN /\ x = ((T` n)` (f` m)))}

Assertion

Ref	Expression
ubthlem3	|- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> (N` ((T` n)` w)) <_ k)

Distinct variable groups:   A,m   C,m   x,m,D   j,n,h,z,y,N   m,n,x,T,j,h,z,y   j,X,z,y   m,Y,x   f,n,j,k,m,h,w,z,y,x

Proof of Theorem ubthlem3

Step	Hyp	Ref	Expression
1		ubthlem3.w	. . 3 |- W e. NrmCVec
2		ubthlem3.2	. . . 4 |- Y = (Base` W)
3		ubthlem3.3	. . . 4 |- N = (norm` W)
4		ubthlem3.9d	. . . 4 |- D = (IndMet` W)
5		fvex 3732	. . . 4 |- ((T` n)` w) e. V
6	2, 3, 4, 5	nvlmle 8333	. . 3 |- (((W e. NrmCVec /\ G:NN-->Y /\ G(~~>m` D)((T` n)` w)) /\ (k e. RR /\ A.g e. NN (N` (G` g)) <_ k)) -> (N` ((T` n)` w)) <_ k)
7	1, 6	mp3anl1 910	. 2 |- (((G:NN-->Y /\ G(~~>m` D)((T` n)` w)) /\ (k e. RR /\ A.g e. NN (N` (G` g)) <_ k)) -> (N` ((T` n)` w)) <_ k)
8		ffvelrn 3814	. . . . . 6 |- (((T` n):X-->Y /\ (f` m) e. X) -> ((T` n)` (f` m)) e. Y)
9		ubthlem3.6	. . . . . . . . . 10 |- T:NN-->B
10	9	ffvelrni 3815	. . . . . . . . 9 |- (n e. NN -> (T` n) e. B)
11		ubthlem3.u	. . . . . . . . . 10 |- U e. NrmCVec
12		ubthlem3.1	. . . . . . . . . . 11 |- X = (Base` U)
13		ubthlem3.5	. . . . . . . . . . 11 |- B = (U BLnOp W)
14	12, 2, 13	blof 8445	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ (T` n) e. B) -> (T` n):X-->Y)
15	11, 1, 14	mp3an12 906	. . . . . . . . 9 |- ((T` n) e. B -> (T` n):X-->Y)
16	10, 15	syl 10	. . . . . . . 8 |- (n e. NN -> (T` n):X-->Y)
17	16	adantl 388	. . . . . . 7 |- ((k e. NN /\ n e. NN) -> (T` n):X-->Y)
18	17	ad2antlr 405	. . . . . 6 |- (((f:NN-->(A` k) /\ (k e. NN /\ n e. NN)) /\ m e. NN) -> (T` n):X-->Y)
19		ffvelrn 3814	. . . . . . . 8 |- ((f:NN-->X /\ m e. NN) -> (f` m) e. X)
20		fss 3635	. . . . . . . . 9 |- ((f:NN-->(A` k) /\ (A` k) (_ X) -> f:NN-->X)
21		ubthlem3.11	. . . . . . . . . 10 |- A = {<.j, y>. | (j e. NN /\ y = {z e. X | A.h e. NN (N` ((T` h)` z)) <_ j})}
22	12, 21	ubthlem2 8530	. . . . . . . . 9 |- (k e. NN -> (A` k) (_ X)
23	20, 22	sylan2 451	. . . . . . . 8 |- ((f:NN-->(A` k) /\ k e. NN) -> f:NN-->X)
24	19, 23	sylan 448	. . . . . . 7 |- (((f:NN-->(A` k) /\ k e. NN) /\ m e. NN) -> (f` m) e. X)
25	24	adantlrr 399	. . . . . 6 |- (((f:NN-->(A` k) /\ (k e. NN /\ n e. NN)) /\ m e. NN) -> (f` m) e. X)
26	8, 18, 25	sylanc 471	. . . . 5 |- (((f:NN-->(A` k) /\ (k e. NN /\ n e. NN)) /\ m e. NN) -> ((T` n)` (f` m)) e. Y)
27	26	adantllr 397	. . . 4 |- ((((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) /\ m e. NN) -> ((T` n)` (f` m)) e. Y)
28	27	r19.21aiva 1714	. . 3 |- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> A.m e. NN ((T` n)` (f` m)) e. Y)
29		ubthlem3.12	. . . 4 |- G = {<.m, x>. | (m e. NN /\ x = ((T` n)` (f` m)))}
30	29	fopab2 3823	. . 3 |- (A.m e. NN ((T` n)` (f` m)) e. Y <-> G:NN-->Y)
31	28, 30	sylib 198	. 2 |- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> G:NN-->Y)
32	4	imsmet 8324	. . . . 5 |- (W e. NrmCVec -> D e. Met)
33	1, 32	ax-mp 7	. . . 4 |- D e. Met
34		ubthlem3.9c	. . . . . . 7 |- C = (IndMet` U)
35	34	imsmet 8324	. . . . . 6 |- (U e. NrmCVec -> C e. Met)
36	11, 35	ax-mp 7	. . . . 5 |- C e. Met
37		eqid 1475	. . . . . 6 |- dom dom C = dom dom C
38		eqid 1475	. . . . . 6 |- (Open` C) = (Open` C)
39		eqid 1475	. . . . . 6 |- (Open` D) = (Open` D)
40		visset 1813	. . . . . 6 |- w e. V
41	37, 38, 39, 29, 40	metcn4i 7972	. . . . 5 |- (((C e. Met /\ D e. Met /\ (T` n) e. ((Open` C) Cn (Open` D))) /\ (f:NN-->dom dom C /\ f(~~>m` C)w)) -> G(~~>m` D)((T` n)` w))
42	36, 41	mp3anl1 910	. . . 4 |- (((D e. Met /\ (T` n) e. ((Open` C) Cn (Open` D))) /\ (f:NN-->dom dom C /\ f(~~>m` C)w)) -> G(~~>m` D)((T` n)` w))
43	33, 42	mpanl1 706	. . 3 |- (((T` n) e. ((Open` C) Cn (Open` D)) /\ (f:NN-->dom dom C /\ f(~~>m` C)w)) -> G(~~>m` D)((T` n)` w))
44	34, 4, 38, 39, 13, 11, 1	blocn2 8468	. . . . 5 |- ((T` n) e. B -> (T` n) e. ((Open` C) Cn (Open` D)))
45	10, 44	syl 10	. . . 4 |- (n e. NN -> (T` n) e. ((Open` C) Cn (Open` D)))
46	45	ad2antll 407	. . 3 |- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> (T` n) e. ((Open` C) Cn (Open` D)))
47	12, 34, 11	imsbai 8322	. . . . . . . 8 |- X = dom dom C
48		feq3 3622	. . . . . . . 8 |- (X = dom dom C -> (f:NN-->X <-> f:NN-->dom dom C))
49	47, 48	ax-mp 7	. . . . . . 7 |- (f:NN-->X <-> f:NN-->dom dom C)
50	23, 49	sylib 198	. . . . . 6 |- ((f:NN-->(A` k) /\ k e. NN) -> f:NN-->dom dom C)
51	50	adantrr 395	. . . . 5 |- ((f:NN-->(A` k) /\ (k e. NN /\ n e. NN)) -> f:NN-->dom dom C)
52	51	anim1i 334	. . . 4 |- (((f:NN-->(A` k) /\ (k e. NN /\ n e. NN)) /\ f(~~>m` C)w) -> (f:NN-->dom dom C /\ f(~~>m` C)w))
53	52	an1rs 489	. . 3 |- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> (f:NN-->dom dom C /\ f(~~>m` C)w))
54	43, 46, 53	sylanc 471	. 2 |- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> G(~~>m` D)((T` n)` w))
55		nnret 5929	. . 3 |- (k e. NN -> k e. RR)
56	55	ad2antrl 406	. 2 |- (((f:NN-->(A` k) /\ f(~~>m` C)w) /\ (k e. NN /\ n e. NN)) -> k e. RR)
57		fveq2 3724	. . . . . . . . 9 |- (m = g -> (f` m) = (f` g))
58	57	fveq2d 3728	. . . . . . . 8 |- (m = g -> ((T` n)` (f` m)) = ((T` n)` (f` g)))
59		fvex 3732	. . . . . . . 8 |- ((T` n)` (f` g)) e. V
60	58, 29, 59	fvopab4 3780	. . . . . . 7 |- (g e. NN -> (G` g) = ((T` n)` (f` g)))
61	60	fveq2d 3728	. . . . . 6 |- (g e. NN -> (N` (G` g)) = (N` ((T` n)` (f` g))))
62	61	adantl 388	. . . . 5 |- (((f:NN-->(A` k) /\ (k e. NN /\ n e. NN)) /\ g e. NN) -> (N` (G` g)) = (N` ((T` n)` (f` g))))
63	12, 21	ubthlem1 8529	. . . . . . . . 9 |- (k e. NN -> ((f` g) e. (A` k) <-> ((f` g) e. X /\ A.n e. NN (N` ((T` n)` (f` g))) <_ k)))
64	63	pm3.27bda 421	. . . . . . . 8 |- ((k e. NN /\ (f` g) e. (A` k)) -> A.n e. NN (N` ((T` n)` (f