# Metamath Proof Explorer

## Definition df-blo

Description: Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007) (New usage is discouraged.)

Ref Expression
Assertion df-blo ${⊢}\mathrm{BLnOp}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({u}\mathrm{LnOp}{w}\right)|\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cblo ${class}\mathrm{BLnOp}$
1 vu ${setvar}{u}$
2 cnv ${class}\mathrm{NrmCVec}$
3 vw ${setvar}{w}$
4 vt ${setvar}{t}$
5 1 cv ${setvar}{u}$
6 clno ${class}\mathrm{LnOp}$
7 3 cv ${setvar}{w}$
8 5 7 6 co ${class}\left({u}\mathrm{LnOp}{w}\right)$
9 cnmoo ${class}{normOp}_{\mathrm{OLD}}$
10 5 7 9 co ${class}\left({u}{normOp}_{\mathrm{OLD}}{w}\right)$
11 4 cv ${setvar}{t}$
12 11 10 cfv ${class}\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)$
13 clt ${class}<$
14 cpnf ${class}\mathrm{+\infty }$
15 12 14 13 wbr ${wff}\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }$
16 15 4 8 crab ${class}\left\{{t}\in \left({u}\mathrm{LnOp}{w}\right)|\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}$
17 1 3 2 2 16 cmpo ${class}\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({u}\mathrm{LnOp}{w}\right)|\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}\right)$
18 0 17 wceq ${wff}\mathrm{BLnOp}=\left({u}\in \mathrm{NrmCVec},{w}\in \mathrm{NrmCVec}⟼\left\{{t}\in \left({u}\mathrm{LnOp}{w}\right)|\left({u}{normOp}_{\mathrm{OLD}}{w}\right)\left({t}\right)<\mathrm{+\infty }\right\}\right)$