MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-blo Structured version   Unicode version

Definition df-blo 22240
Description: Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-blo  |-  BLnOp  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { t  e.  ( u  LnOp  w
)  |  ( ( u normOp OLD w ) `  t )  <  +oo } )
Distinct variable group:    u, t, w

Detailed syntax breakdown of Definition df-blo
StepHypRef Expression
1 cblo 22236 . 2  class  BLnOp
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 22056 . . 3  class  NrmCVec
5 vt . . . . . . 7  set  t
65cv 1651 . . . . . 6  class  t
72cv 1651 . . . . . . 7  class  u
83cv 1651 . . . . . . 7  class  w
9 cnmoo 22235 . . . . . . 7  class  normOp OLD
107, 8, 9co 6074 . . . . . 6  class  ( u
normOp OLD w )
116, 10cfv 5447 . . . . 5  class  ( ( u normOp OLD w ) `  t )
12 cpnf 9110 . . . . 5  class  +oo
13 clt 9113 . . . . 5  class  <
1411, 12, 13wbr 4205 . . . 4  wff  ( ( u normOp OLD w ) `  t )  <  +oo
15 clno 22234 . . . . 5  class  LnOp
167, 8, 15co 6074 . . . 4  class  ( u 
LnOp  w )
1714, 5, 16crab 2702 . . 3  class  { t  e.  ( u  LnOp  w )  |  ( ( u normOp OLD w ) `  t )  <  +oo }
182, 3, 4, 4, 17cmpt2 6076 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  { t  e.  ( u  LnOp  w )  |  ( ( u
normOp OLD w ) `  t )  <  +oo } )
191, 18wceq 1652 1  wff  BLnOp  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { t  e.  ( u  LnOp  w
)  |  ( ( u normOp OLD w ) `  t )  <  +oo } )
Colors of variables: wff set class
This definition is referenced by:  bloval  22275
  Copyright terms: Public domain W3C validator