Theorem nmounbseqi

Description: An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-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	nmounbseqi	|- ( ( T : X --> Y /\ ( N ` T ) = +oo ) -> E. f ( f : NN --> X /\ A. k e. NN ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )

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	1 2 3 4 5 6 7	nmounbi	|- ( T : X --> Y -> ( ( N ` T ) = +oo <-> A. k e. RR E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) ) )
9	8	biimpa	|- ( ( T : X --> Y /\ ( N ` T ) = +oo ) -> A. k e. RR E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) )
10		nnre	|- ( k e. NN -> k e. RR )
11	10	imim1i	|- ( ( k e. RR -> E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) ) -> ( k e. NN -> E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) ) )
12	11	ralimi2	|- ( A. k e. RR E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) -> A. k e. NN E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) )
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	breq2d	|- ( y = ( f ` k ) -> ( k < ( M ` ( T ` y ) ) <-> k < ( M ` ( T ` ( f ` k ) ) ) ) )
19	16 18	anbi12d	|- ( y = ( f ` k ) -> ( ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) <-> ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )
20	13 14 19	axcc4	|- ( A. k e. NN E. y e. X ( ( L ` y ) <_ 1 /\ k < ( M ` ( T ` y ) ) ) -> E. f ( f : NN --> X /\ A. k e. NN ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )
21	9 12 20	3syl	|- ( ( T : X --> Y /\ ( N ` T ) = +oo ) -> E. f ( f : NN --> X /\ A. k e. NN ( ( L ` ( f ` k ) ) <_ 1 /\ k < ( M ` ( T ` ( f ` k ) ) ) ) ) )