# Metamath Proof Explorer

## Theorem blof

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

Ref Expression
Hypotheses blof.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
blof.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
blof.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
Assertion blof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}:{X}⟶{Y}$

### Proof

Step Hyp Ref Expression
1 blof.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 blof.2 ${⊢}{Y}=\mathrm{BaseSet}\left({W}\right)$
3 blof.5 ${⊢}{B}={U}\mathrm{BLnOp}{W}$
4 eqid ${⊢}{U}\mathrm{LnOp}{W}={U}\mathrm{LnOp}{W}$
5 4 3 bloln ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}\in \left({U}\mathrm{LnOp}{W}\right)$
6 1 2 4 lnof ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in \left({U}\mathrm{LnOp}{W}\right)\right)\to {T}:{X}⟶{Y}$
7 5 6 syld3an3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {W}\in \mathrm{NrmCVec}\wedge {T}\in {B}\right)\to {T}:{X}⟶{Y}$