Definition df-bdop

Description: Define the set of bounded linear Hilbert space operators. (See df-hosum for definition of operator.) (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-bdop	$$⊢\mathrm{BndLinOp}=\left\{t\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(t\right)<\mathrm{+\infty }\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbo	$$class\mathrm{BndLinOp}$$
1		vt	$$setvart$$
2		clo	$$class\mathrm{LinOp}$$
3		cnop	$$class{norm}_{\mathrm{op}}$$
4	1	cv	$$setvart$$
5	4 3	cfv	$$class{norm}_{\mathrm{op}}\left(t\right)$$
6		clt	$$class<$$
7		cpnf	$$class\mathrm{+\infty }$$
8	5 7 6	wbr	$$wff{norm}_{\mathrm{op}}\left(t\right)<\mathrm{+\infty }$$
9	8 1 2	crab	$$class\left\{t\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(t\right)<\mathrm{+\infty }\right\}$$
10	0 9	wceq	$$wff\mathrm{BndLinOp}=\left\{t\in \mathrm{LinOp}|{norm}_{\mathrm{op}}\left(t\right)<\mathrm{+\infty }\right\}$$