Description: Property defining a bounded linear Hilbert space operator. (Contributed by NM, 18-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elbdop | |- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 | |- ( t = T -> ( normop ` t ) = ( normop ` T ) ) |
|
| 2 | 1 | breq1d | |- ( t = T -> ( ( normop ` t ) < +oo <-> ( normop ` T ) < +oo ) ) |
| 3 | df-bdop | |- BndLinOp = { t e. LinOp | ( normop ` t ) < +oo } |
|
| 4 | 2 3 | elrab2 | |- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) < +oo ) ) |