# Metamath Proof Explorer

## Theorem bloln

Description: A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses bloln.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
bloln.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
Assertion bloln ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}\in {L}$

### Proof

Step Hyp Ref Expression
1 bloln.4 ${⊢}{L}={U}\mathrm{LnOp}{W}$
2 bloln.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
3 eqid ${⊢}{U}{normOp}_{\mathrm{OLD}}{W}={U}{normOp}_{\mathrm{OLD}}{W}$
4 3 1 2 isblo ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left({T}\in {B}↔\left({T}\in {L}\wedge \left({U}{normOp}_{\mathrm{OLD}}{W}\right)\left({T}\right)<\mathrm{+\infty }\right)\right)$
5 4 simprbda ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {T}\in {B}\right)\to {T}\in {L}$
6 5 3impa ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}\in {L}$