Metamath Proof Explorer

Theorem blocni

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of Kreyszig p. 97. (Contributed by NM, 18-Dec-2007) (Revised by Mario Carneiro, 10-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses blocni.8 
|- C = ( IndMet ` U )
blocni.d 
|- D = ( IndMet ` W )
blocni.j 
|- J = ( MetOpen ` C )
blocni.k 
|- K = ( MetOpen ` 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
Assertion blocni 
|- ( T e. ( J Cn K ) <-> T e. B )

Proof

Step Hyp Ref Expression
1 blocni.8 
 |-  C = ( IndMet ` U )
2 blocni.d 
 |-  D = ( IndMet ` W )
3 blocni.j 
 |-  J = ( MetOpen ` C )
4 blocni.k 
 |-  K = ( MetOpen ` D )
5 blocni.4 
 |-  L = ( U LnOp W )
6 blocni.5 
 |-  B = ( U BLnOp W )
7 blocni.u 
 |-  U e. NrmCVec
8 blocni.w 
 |-  W e. NrmCVec
9 blocni.l 
 |-  T e. L
10 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
11 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
12 10 11 nvzcl 
 |-  ( U e. NrmCVec -> ( 0vec ` U ) e. ( BaseSet ` U ) )
13 7 12 ax-mp 
 |-  ( 0vec ` U ) e. ( BaseSet ` U )
14 10 1 imsmet 
 |-  ( U e. NrmCVec -> C e. ( Met ` ( BaseSet ` U ) ) )
15 7 14 ax-mp 
 |-  C e. ( Met ` ( BaseSet ` U ) )
16 metxmet 
 |-  ( C e. ( Met ` ( BaseSet ` U ) ) -> C e. ( *Met ` ( BaseSet ` U ) ) )
17 15 16 ax-mp 
 |-  C e. ( *Met ` ( BaseSet ` U ) )
18 3 mopntopon 
 |-  ( C e. ( *Met ` ( BaseSet ` U ) ) -> J e. ( TopOn ` ( BaseSet ` U ) ) )
19 17 18 ax-mp 
 |-  J e. ( TopOn ` ( BaseSet ` U ) )
20 19 toponunii 
 |-  ( BaseSet ` U ) = U. J
21 20 cncnpi 
 |-  ( ( T e. ( J Cn K ) /\ ( 0vec ` U ) e. ( BaseSet ` U ) ) -> T e. ( ( J CnP K ) ` ( 0vec ` U ) ) )
22 13 21 mpan2 
 |-  ( T e. ( J Cn K ) -> T e. ( ( J CnP K ) ` ( 0vec ` U ) ) )
23 1 2 3 4 5 6 7 8 9 10 blocnilem 
 |-  ( ( ( 0vec ` U ) e. ( BaseSet ` U ) /\ T e. ( ( J CnP K ) ` ( 0vec ` U ) ) ) -> T e. B )
24 13 22 23 sylancr 
 |-  ( T e. ( J Cn K ) -> T e. B )
25 eleq1 
 |-  ( T = ( U 0op W ) -> ( T e. ( J Cn K ) <-> ( U 0op W ) e. ( J Cn K ) ) )
26 simprr 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> y e. RR+ )
27 eqid 
 |-  ( BaseSet ` W ) = ( BaseSet ` W )
28 eqid 
 |-  ( U normOpOLD W ) = ( U normOpOLD W )
29 10 27 28 6 nmblore 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. B ) -> ( ( U normOpOLD W ) ` T ) e. RR )
30 7 8 29 mp3an12 
 |-  ( T e. B -> ( ( U normOpOLD W ) ` T ) e. RR )
31 eqid 
 |-  ( U 0op W ) = ( U 0op W )
32 28 31 5 nmlnogt0 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> ( T =/= ( U 0op W ) <-> 0 < ( ( U normOpOLD W ) ` T ) ) )
33 7 8 9 32 mp3an 
 |-  ( T =/= ( U 0op W ) <-> 0 < ( ( U normOpOLD W ) ` T ) )
34 33 biimpi 
 |-  ( T =/= ( U 0op W ) -> 0 < ( ( U normOpOLD W ) ` T ) )
35 30 34 anim12i 
 |-  ( ( T e. B /\ T =/= ( U 0op W ) ) -> ( ( ( U normOpOLD W ) ` T ) e. RR /\ 0 < ( ( U normOpOLD W ) ` T ) ) )
36 elrp 
 |-  ( ( ( U normOpOLD W ) ` T ) e. RR+ <-> ( ( ( U normOpOLD W ) ` T ) e. RR /\ 0 < ( ( U normOpOLD W ) ` T ) ) )
37 35 36 sylibr 
 |-  ( ( T e. B /\ T =/= ( U 0op W ) ) -> ( ( U normOpOLD W ) ` T ) e. RR+ )
38 37 adantr 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> ( ( U normOpOLD W ) ` T ) e. RR+ )
39 26 38 rpdivcld 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> ( y / ( ( U normOpOLD W ) ` T ) ) e. RR+ )
40 simprl 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> x e. ( BaseSet ` U ) )
41 metcl 
 |-  ( ( C e. ( Met ` ( BaseSet ` U ) ) /\ x e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( x C w ) e. RR )
42 15 41 mp3an1 
 |-  ( ( x e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( x C w ) e. RR )
43 40 42 sylan 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( x C w ) e. RR )
44 simplrr 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> y e. RR+ )
45 44 rpred 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> y e. RR )
46 35 ad2antrr 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( U normOpOLD W ) ` T ) e. RR /\ 0 < ( ( U normOpOLD W ) ` T ) ) )
47 ltmuldiv2 
 |-  ( ( ( x C w ) e. RR /\ y e. RR /\ ( ( ( U normOpOLD W ) ` T ) e. RR /\ 0 < ( ( U normOpOLD W ) ` T ) ) ) -> ( ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) < y <-> ( x C w ) < ( y / ( ( U normOpOLD W ) ` T ) ) ) )
48 43 45 46 47 syl3anc 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) < y <-> ( x C w ) < ( y / ( ( U normOpOLD W ) ` T ) ) ) )
49 id 
 |-  ( ( T e. B /\ x e. ( BaseSet ` U ) ) -> ( T e. B /\ x e. ( BaseSet ` U ) ) )
50 49 ad2ant2r 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> ( T e. B /\ x e. ( BaseSet ` U ) ) )
51 10 27 1 2 28 6 7 8 blometi 
 |-  ( ( T e. B /\ x e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( ( T ` x ) D ( T ` w ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) )
52 51 3expa 
 |-  ( ( ( T e. B /\ x e. ( BaseSet ` U ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( T ` x ) D ( T ` w ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) )
53 50 52 sylan 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( T ` x ) D ( T ` w ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) )
54 10 27 5 lnof 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec /\ T e. L ) -> T : ( BaseSet ` U ) --> ( BaseSet ` W ) )
55 7 8 9 54 mp3an 
 |-  T : ( BaseSet ` U ) --> ( BaseSet ` W )
56 55 ffvelrni 
 |-  ( x e. ( BaseSet ` U ) -> ( T ` x ) e. ( BaseSet ` W ) )
57 55 ffvelrni 
 |-  ( w e. ( BaseSet ` U ) -> ( T ` w ) e. ( BaseSet ` W ) )
58 27 2 imsmet 
 |-  ( W e. NrmCVec -> D e. ( Met ` ( BaseSet ` W ) ) )
59 8 58 ax-mp 
 |-  D e. ( Met ` ( BaseSet ` W ) )
60 metcl 
 |-  ( ( D e. ( Met ` ( BaseSet ` W ) ) /\ ( T ` x ) e. ( BaseSet ` W ) /\ ( T ` w ) e. ( BaseSet ` W ) ) -> ( ( T ` x ) D ( T ` w ) ) e. RR )
61 59 60 mp3an1 
 |-  ( ( ( T ` x ) e. ( BaseSet ` W ) /\ ( T ` w ) e. ( BaseSet ` W ) ) -> ( ( T ` x ) D ( T ` w ) ) e. RR )
62 56 57 61 syl2an 
 |-  ( ( x e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) -> ( ( T ` x ) D ( T ` w ) ) e. RR )
63 40 62 sylan 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( T ` x ) D ( T ` w ) ) e. RR )
64 remulcl 
 |-  ( ( ( ( U normOpOLD W ) ` T ) e. RR /\ ( x C w ) e. RR ) -> ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) e. RR )
65 30 42 64 syl2an 
 |-  ( ( T e. B /\ ( x e. ( BaseSet ` U ) /\ w e. ( BaseSet ` U ) ) ) -> ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) e. RR )
66 65 anassrs 
 |-  ( ( ( T e. B /\ x e. ( BaseSet ` U ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) e. RR )
67 66 adantllr 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ x e. ( BaseSet ` U ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) e. RR )
68 67 adantlrr 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) e. RR )
69 lelttr 
 |-  ( ( ( ( T ` x ) D ( T ` w ) ) e. RR /\ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) e. RR /\ y e. RR ) -> ( ( ( ( T ` x ) D ( T ` w ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) /\ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) < y ) -> ( ( T ` x ) D ( T ` w ) ) < y ) )
70 63 68 45 69 syl3anc 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( ( T ` x ) D ( T ` w ) ) <_ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) /\ ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) < y ) -> ( ( T ` x ) D ( T ` w ) ) < y ) )
71 53 70 mpand 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( ( ( U normOpOLD W ) ` T ) x. ( x C w ) ) < y -> ( ( T ` x ) D ( T ` w ) ) < y ) )
72 48 71 sylbird 
 |-  ( ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) /\ w e. ( BaseSet ` U ) ) -> ( ( x C w ) < ( y / ( ( U normOpOLD W ) ` T ) ) -> ( ( T ` x ) D ( T ` w ) ) < y ) )
73 72 ralrimiva 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> A. w e. ( BaseSet ` U ) ( ( x C w ) < ( y / ( ( U normOpOLD W ) ` T ) ) -> ( ( T ` x ) D ( T ` w ) ) < y ) )
74 breq2 
 |-  ( z = ( y / ( ( U normOpOLD W ) ` T ) ) -> ( ( x C w ) < z <-> ( x C w ) < ( y / ( ( U normOpOLD W ) ` T ) ) ) )
75 74 rspceaimv 
 |-  ( ( ( y / ( ( U normOpOLD W ) ` T ) ) e. RR+ /\ A. w e. ( BaseSet ` U ) ( ( x C w ) < ( y / ( ( U normOpOLD W ) ` T ) ) -> ( ( T ` x ) D ( T ` w ) ) < y ) ) -> E. z e. RR+ A. w e. ( BaseSet ` U ) ( ( x C w ) < z -> ( ( T ` x ) D ( T ` w ) ) < y ) )
76 39 73 75 syl2anc 
 |-  ( ( ( T e. B /\ T =/= ( U 0op W ) ) /\ ( x e. ( BaseSet ` U ) /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. ( BaseSet ` U ) ( ( x C w ) < z -> ( ( T ` x ) D ( T ` w ) ) < y ) )
77 76 ralrimivva 
 |-  ( ( T e. B /\ T =/= ( U 0op W ) ) -> A. x e. ( BaseSet ` U ) A. y e. RR+ E. z e. RR+ A. w e. ( BaseSet ` U ) ( ( x C w ) < z -> ( ( T ` x ) D ( T ` w ) ) < y ) )
78 77 55 jctil 
 |-  ( ( T e. B /\ T =/= ( U 0op W ) ) -> ( T : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ A. x e. ( BaseSet ` U ) A. y e. RR+ E. z e. RR+ A. w e. ( BaseSet ` U ) ( ( x C w ) < z -> ( ( T ` x ) D ( T ` w ) ) < y ) ) )
79 metxmet 
 |-  ( D e. ( Met ` ( BaseSet ` W ) ) -> D e. ( *Met ` ( BaseSet ` W ) ) )
80 59 79 ax-mp 
 |-  D e. ( *Met ` ( BaseSet ` W ) )
81 3 4 metcn 
 |-  ( ( C e. ( *Met ` ( BaseSet ` U ) ) /\ D e. ( *Met ` ( BaseSet ` W ) ) ) -> ( T e. ( J Cn K ) <-> ( T : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ A. x e. ( BaseSet ` U ) A. y e. RR+ E. z e. RR+ A. w e. ( BaseSet ` U ) ( ( x C w ) < z -> ( ( T ` x ) D ( T ` w ) ) < y ) ) ) )
82 17 80 81 mp2an 
 |-  ( T e. ( J Cn K ) <-> ( T : ( BaseSet ` U ) --> ( BaseSet ` W ) /\ A. x e. ( BaseSet ` U ) A. y e. RR+ E. z e. RR+ A. w e. ( BaseSet ` U ) ( ( x C w ) < z -> ( ( T ` x ) D ( T ` w ) ) < y ) ) )
83 78 82 sylibr 
 |-  ( ( T e. B /\ T =/= ( U 0op W ) ) -> T e. ( J Cn K ) )
84 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
85 10 84 31 0ofval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U 0op W ) = ( ( BaseSet ` U ) X. { ( 0vec ` W ) } ) )
86 7 8 85 mp2an 
 |-  ( U 0op W ) = ( ( BaseSet ` U ) X. { ( 0vec ` W ) } )
87 4 mopntopon 
 |-  ( D e. ( *Met ` ( BaseSet ` W ) ) -> K e. ( TopOn ` ( BaseSet ` W ) ) )
88 80 87 ax-mp 
 |-  K e. ( TopOn ` ( BaseSet ` W ) )
89 27 84 nvzcl 
 |-  ( W e. NrmCVec -> ( 0vec ` W ) e. ( BaseSet ` W ) )
90 8 89 ax-mp 
 |-  ( 0vec ` W ) e. ( BaseSet ` W )
91 cnconst2 
 |-  ( ( J e. ( TopOn ` ( BaseSet ` U ) ) /\ K e. ( TopOn ` ( BaseSet ` W ) ) /\ ( 0vec ` W ) e. ( BaseSet ` W ) ) -> ( ( BaseSet ` U ) X. { ( 0vec ` W ) } ) e. ( J Cn K ) )
92 19 88 90 91 mp3an 
 |-  ( ( BaseSet ` U ) X. { ( 0vec ` W ) } ) e. ( J Cn K )
93 86 92 eqeltri 
 |-  ( U 0op W ) e. ( J Cn K )
94 93 a1i 
 |-  ( T e. B -> ( U 0op W ) e. ( J Cn K ) )
95 25 83 94 pm2.61ne 
 |-  ( T e. B -> T e. ( J Cn K ) )
96 24 95 impbii 
 |-  ( T e. ( J Cn K ) <-> T e. B )