This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrrid 
 |-  ( 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 )