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	|- BLnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cblo	|- BLnOp
1		vu	|- u
2		cnv	|- NrmCVec
3		vw	|- w
4		vt	|- t
5	1	cv	|- u
6		clno	|- LnOp
7	3	cv	|- w
8	5 7 6	co	|- ( u LnOp w )
9		cnmoo	|- normOpOLD
10	5 7 9	co	|- ( u normOpOLD w )
11	4	cv	|- t
12	11 10	cfv	|- ( ( u normOpOLD w ) ` t )
13		clt	|- <
14		cpnf	|- +oo
15	12 14 13	wbr	|- ( ( u normOpOLD w ) ` t ) < +oo
16	15 4 8	crab	|- { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo }
17	1 3 2 2 16	cmpo	|- ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )
18	0 17	wceq	|- BLnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )