# Metamath Proof Explorer

## Theorem isblo

Description: The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses bloval.3
`|- N = ( U normOpOLD W )`
bloval.4
`|- L = ( U LnOp W )`
bloval.5
`|- B = ( U BLnOp W )`
Assertion isblo
`|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( N ` T ) < +oo ) ) )`

### Proof

Step Hyp Ref Expression
1 bloval.3
` |-  N = ( U normOpOLD W )`
2 bloval.4
` |-  L = ( U LnOp W )`
3 bloval.5
` |-  B = ( U BLnOp W )`
4 1 2 3 bloval
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> B = { t e. L | ( N ` t ) < +oo } )`
5 4 eleq2d
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> T e. { t e. L | ( N ` t ) < +oo } ) )`
6 fveq2
` |-  ( t = T -> ( N ` t ) = ( N ` T ) )`
7 6 breq1d
` |-  ( t = T -> ( ( N ` t ) < +oo <-> ( N ` T ) < +oo ) )`
8 7 elrab
` |-  ( T e. { t e. L | ( N ` t ) < +oo } <-> ( T e. L /\ ( N ` T ) < +oo ) )`
9 5 8 syl6bb
` |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( T e. B <-> ( T e. L /\ ( N ` T ) < +oo ) ) )`