Theorem nmobndseqi

Description: A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008) (Revised by Mario Carneiro, 7-Apr-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmoubi.1	|- X = ( BaseSet ` U )
	nmoubi.y	|- Y = ( BaseSet ` W )
	nmoubi.l	|- L = ( normCV ` U )
	nmoubi.m	|- M = ( normCV ` W )
	nmoubi.3	|- N = ( U normOpOLD W )
	nmoubi.u	|- U e. NrmCVec
	nmoubi.w	|- W e. NrmCVec
Assertion	nmobndseqi	|- ( ( T : X --> Y /\ A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> ( N ` T ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		nmoubi.1	|- X = ( BaseSet ` U )
2		nmoubi.y	|- Y = ( BaseSet ` W )
3		nmoubi.l	|- L = ( normCV ` U )
4		nmoubi.m	|- M = ( normCV ` W )
5		nmoubi.3	|- N = ( U normOpOLD W )
6		nmoubi.u	|- U e. NrmCVec
7		nmoubi.w	|- W e. NrmCVec
8		impexp	|- ( ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> ( f : NN --> X -> ( A. k e. NN ( L ` ( f ` k ) ) <_ 1 -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
9		r19.35	|- ( E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> ( A. k e. NN ( L ` ( f ` k ) ) <_ 1 -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) )
10	9	imbi2i	|- ( ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) <-> ( f : NN --> X -> ( A. k e. NN ( L ` ( f ` k ) ) <_ 1 -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
11	8 10	bitr4i	|- ( ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
12	11	albii	|- ( A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
13	1	fvexi	|- X e. _V
14		nnenom	|- NN ~~ _om
15		fveq2	|- ( y = ( f ` k ) -> ( L ` y ) = ( L ` ( f ` k ) ) )
16	15	breq1d	|- ( y = ( f ` k ) -> ( ( L ` y ) <_ 1 <-> ( L ` ( f ` k ) ) <_ 1 ) )
17		2fveq3	|- ( y = ( f ` k ) -> ( M ` ( T ` y ) ) = ( M ` ( T ` ( f ` k ) ) ) )
18	17	breq1d	|- ( y = ( f ` k ) -> ( ( M ` ( T ` y ) ) <_ k <-> ( M ` ( T ` ( f ` k ) ) ) <_ k ) )
19	16 18	imbi12d	|- ( y = ( f ` k ) -> ( ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
20	19	notbid	|- ( y = ( f ` k ) -> ( -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
21	13 14 20	axcc4	|- ( A. k e. NN E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) -> E. f ( f : NN --> X /\ A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
22	21	con3i	|- ( -. E. f ( f : NN --> X /\ A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> -. A. k e. NN E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
23		dfrex2	|- ( E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) <-> -. A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) )
24	23	imbi2i	|- ( ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) <-> ( f : NN --> X -> -. A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
25	24	albii	|- ( A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) <-> A. f ( f : NN --> X -> -. A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
26		alinexa	|- ( A. f ( f : NN --> X -> -. A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) <-> -. E. f ( f : NN --> X /\ A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
27	25 26	bitri	|- ( A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) <-> -. E. f ( f : NN --> X /\ A. k e. NN -. ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) )
28		dfral2	|- ( A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> -. E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
29	28	rexbii	|- ( E. k e. NN A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> E. k e. NN -. E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
30		rexnal	|- ( E. k e. NN -. E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> -. A. k e. NN E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
31	29 30	bitri	|- ( E. k e. NN A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) <-> -. A. k e. NN E. y e. X -. ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
32	22 27 31	3imtr4i	|- ( A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> E. k e. NN A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
33		nnre	|- ( k e. NN -> k e. RR )
34	33	anim1i	|- ( ( k e. NN /\ A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) ) -> ( k e. RR /\ A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) ) )
35	34	reximi2	|- ( E. k e. NN A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) -> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
36	32 35	syl	|- ( A. f ( f : NN --> X -> E. k e. NN ( ( L ` ( f ` k ) ) <_ 1 -> ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
37	12 36	sylbi	|- ( A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) -> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) )
38	1 2 3 4 5 6 7	nmobndi	|- ( T : X --> Y -> ( ( N ` T ) e. RR <-> E. k e. RR A. y e. X ( ( L ` y ) <_ 1 -> ( M ` ( T ` y ) ) <_ k ) ) )
39	37 38	syl5ibr	|- ( T : X --> Y -> ( A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) -> ( N ` T ) e. RR ) )
40	39	imp	|- ( ( T : X --> Y /\ A. f ( ( f : NN --> X /\ A. k e. NN ( L ` ( f ` k ) ) <_ 1 ) -> E. k e. NN ( M ` ( T ` ( f ` k ) ) ) <_ k ) ) -> ( N ` T ) e. RR )