# 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}{normOp}_{\mathrm{OLD}}{W}$
bloval.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
bloval.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
Assertion isblo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {B}↔\left({T}\in {L}\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)\right)$

### Proof

Step Hyp Ref Expression
1 bloval.3 ${⊢}{N}={U}{normOp}_{\mathrm{OLD}}{W}$
2 bloval.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
3 bloval.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
4 1 2 3 bloval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to {B}=\left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}$
5 4 eleq2d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {B}↔{T}\in \left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}\right)$
6 fveq2 ${⊢}{t}={T}\to {N}\left({t}\right)={N}\left({T}\right)$
7 6 breq1d ${⊢}{t}={T}\to \left({N}\left({t}\right)<\mathrm{+\infty }↔{N}\left({T}\right)<\mathrm{+\infty }\right)$
8 7 elrab ${⊢}{T}\in \left\{{t}\in {L}|{N}\left({t}\right)<\mathrm{+\infty }\right\}↔\left({T}\in {L}\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)$
9 5 8 syl6bb ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {B}↔\left({T}\in {L}\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)\right)$