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 } |
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 } |