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

Definition df-blo 21324
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 21320 . 2  class  BLnOp
2 vu . . 3  set  u
3 vw . . 3  set  w
4 cnv 21140 . . 3  class  NrmCVec
5 vt . . . . . . 7  set  t
65cv 1622 . . . . . 6  class  t
72cv 1622 . . . . . . 7  class  u
83cv 1622 . . . . . . 7  class  w
9 cnmoo 21319 . . . . . . 7  class  normOp OLD
107, 8, 9co 5858 . . . . . 6  class  ( u
normOp OLD w )
116, 10cfv 5255 . . . . 5  class  ( ( u normOp OLD w ) `  t )
12 cpnf 8864 . . . . 5  class  +oo
13 clt 8867 . . . . 5  class  <
1411, 12, 13wbr 4023 . . . 4  wff  ( ( u normOp OLD w ) `  t )  <  +oo
15 clno 21318 . . . . 5  class  LnOp
167, 8, 15co 5858 . . . 4  class  ( u 
LnOp  w )
1714, 5, 16crab 2547 . . 3  class  { t  e.  ( u  LnOp  w )  |  ( ( u normOp OLD w ) `  t )  <  +oo }
182, 3, 4, 4, 17cmpt2 5860 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  { t  e.  ( u  LnOp  w )  |  ( ( u
normOp OLD w ) `  t )  <  +oo } )
191, 18wceq 1623 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  21359
  Copyright terms: Public domain W3C validator