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

Definition df-blo 24283
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 normOpOLD w ) `  t )  < +oo } )
Distinct variable group:    u, t, w

Detailed syntax breakdown of Definition df-blo
StepHypRef Expression
1 cblo 24279 . 2  class  BLnOp
2 vu . . 3  setvar  u
3 vw . . 3  setvar  w
4 cnv 24099 . . 3  class  NrmCVec
5 vt . . . . . . 7  setvar  t
65cv 1369 . . . . . 6  class  t
72cv 1369 . . . . . . 7  class  u
83cv 1369 . . . . . . 7  class  w
9 cnmoo 24278 . . . . . . 7  class  normOpOLD
107, 8, 9co 6192 . . . . . 6  class  ( u
normOpOLD w )
116, 10cfv 5518 . . . . 5  class  ( ( u normOpOLD w ) `  t )
12 cpnf 9518 . . . . 5  class +oo
13 clt 9521 . . . . 5  class  <
1411, 12, 13wbr 4392 . . . 4  wff  ( ( u normOpOLD w ) `  t )  < +oo
15 clno 24277 . . . . 5  class  LnOp
167, 8, 15co 6192 . . . 4  class  ( u 
LnOp  w )
1714, 5, 16crab 2799 . . 3  class  { t  e.  ( u  LnOp  w )  |  ( ( u normOpOLD w ) `  t )  < +oo }
182, 3, 4, 4, 17cmpt2 6194 . 2  class  ( u  e.  NrmCVec ,  w  e.  NrmCVec 
|->  { t  e.  ( u  LnOp  w )  |  ( ( u
normOpOLD w ) `  t )  < +oo } )
191, 18wceq 1370 1  wff  BLnOp  =  ( u  e.  NrmCVec ,  w  e.  NrmCVec  |->  { t  e.  ( u  LnOp  w
)  |  ( ( u normOpOLD w ) `  t )  < +oo } )
Colors of variables: wff setvar class
This definition is referenced by:  bloval  24318
  Copyright terms: Public domain W3C validator