Definition df-blo 27601

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

Assertion

Ref	Expression
df-blo	|- BLnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )

Distinct variable group:   u, t, w

Detailed syntax breakdown of Definition df-blo

Step	Hyp	Ref	Expression
1		cblo 27597	. 2 class BLnOp
2		vu	. . 3 setvar u
3		vw	. . 3 setvar w
4		cnv 27439	. . 3 class NrmCVec
5		vt	. . . . . . 7 setvar t
6	5	cv 1482	. . . . . 6 class t
7	2	cv 1482	. . . . . . 7 class u
8	3	cv 1482	. . . . . . 7 class w
9		cnmoo 27596	. . . . . . 7 class normOpOLD
10	7, 8, 9	co 6650	. . . . . 6 class ( u normOpOLD w )
11	6, 10	cfv 5888	. . . . 5 class ( ( u normOpOLD w ) ` t )
12		cpnf 10071	. . . . 5 class +oo
13		clt 10074	. . . . 5 class <
14	11, 12, 13	wbr 4653	. . . 4 wff ( ( u normOpOLD w ) ` t ) < +oo
15		clno 27595	. . . . 5 class LnOp
16	7, 8, 15	co 6650	. . . 4 class ( u LnOp w )
17	14, 5, 16	crab 2916	. . 3 class { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo }
18	2, 3, 4, 4, 17	cmpt2 6652	. 2 class ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )
19	1, 18	wceq 1483	1 wff BLnOp = ( u e. NrmCVec , w e. NrmCVec |-> { t e. ( u LnOp w ) | ( ( u normOpOLD w ) ` t ) < +oo } )

This definition is referenced by:  bloval  27636