# Metamath Proof Explorer

## Theorem isblo2

Description: The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-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 isblo2 ${⊢}\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)\in ℝ\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 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)$
5 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
6 eqid ${⊢}\mathrm{BaseSet}\left({W}\right)=\mathrm{BaseSet}\left({W}\right)$
7 5 6 2 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to {T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)$
8 5 6 1 nmoreltpnf ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}:\mathrm{BaseSet}\left({U}\right)⟶\mathrm{BaseSet}\left({W}\right)\right)\to \left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)<\mathrm{+\infty }\right)$
9 7 8 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {L}\right)\to \left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)<\mathrm{+\infty }\right)$
10 9 3expa ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\wedge {T}\in {L}\right)\to \left({N}\left({T}\right)\in ℝ↔{N}\left({T}\right)<\mathrm{+\infty }\right)$
11 10 pm5.32da ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\right)\to \left(\left({T}\in {L}\wedge {N}\left({T}\right)\in ℝ\right)↔\left({T}\in {L}\wedge {N}\left({T}\right)<\mathrm{+\infty }\right)\right)$
12 4 11 bitr4d ${⊢}\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)\in ℝ\right)\right)$