Metamath Proof Explorer


Definition df-bdop

Description: Define the set of bounded linear Hilbert space operators. (See df-hosum for definition of operator.) (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion df-bdop
|- BndLinOp = { t e. LinOp | ( normop ` t ) < +oo }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbo
 |-  BndLinOp
1 vt
 |-  t
2 clo
 |-  LinOp
3 cnop
 |-  normop
4 1 cv
 |-  t
5 4 3 cfv
 |-  ( normop ` t )
6 clt
 |-  <
7 cpnf
 |-  +oo
8 5 7 6 wbr
 |-  ( normop ` t ) < +oo
9 8 1 2 crab
 |-  { t e. LinOp | ( normop ` t ) < +oo }
10 0 9 wceq
 |-  BndLinOp = { t e. LinOp | ( normop ` t ) < +oo }