Definition df-blo 9746

Description: Define the class of bounded linear operators between two normed complex vector spaces.

Assertion

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

Distinct variable group:   t,o,u,w

Detailed syntax breakdown of Definition df-blo

Step	Hyp	Ref	Expression
1		cblo 9742	. 2 class BLnOp
2		vu	. . . . . . 7 set u
3	2	cv 1297	. . . . . 6 class u
4		cnv 9535	. . . . . 6 class NrmCVec
5	3, 4	wcel 1300	. . . . 5 wff u e. NrmCVec
6		vw	. . . . . . 7 set w
7	6	cv 1297	. . . . . 6 class w
8	7, 4	wcel 1300	. . . . 5 wff w e. NrmCVec
9	5, 8	wa 240	. . . 4 wff (u e. NrmCVec /\ w e. NrmCVec)
10		vo	. . . . . 6 set o
11	10	cv 1297	. . . . 5 class o
12		vt	. . . . . . . . 9 set t
13	12	cv 1297	. . . . . . . 8 class t
14		cnmo 9741	. . . . . . . . 9 class normOp
15	3, 7, 14	co 4884	. . . . . . . 8 class (unormOpw)
16	13, 15	cfv 3998	. . . . . . 7 class ((unormOpw)` t)
17		cpnf 6650	. . . . . . 7 class +oo
18		clt 6653	. . . . . . 7 class <
19	16, 17, 18	wbr 3338	. . . . . 6 wff ((unormOpw)` t) < +oo
20		clno 9740	. . . . . . 7 class LnOp
21	3, 7, 20	co 4884	. . . . . 6 class (u LnOp w)
22	19, 12, 21	crab 2108	. . . . 5 class {t e. (u LnOp w) | ((unormOpw)` t) < +oo}
23	11, 22	wceq 1298	. . . 4 wff o = {t e. (u LnOp w) | ((unormOpw)` t) < +oo}
24	9, 23	wa 240	. . 3 wff ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t e. (u LnOp w) | ((unormOpw)` t) < +oo})
25	24, 2, 6, 10	copab2 4885	. 2 class {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t e. (u LnOp w) | ((unormOpw)` t) < +oo})}
26	1, 25	wceq 1298	1 wff BLnOp = {<.<.u, w>., o>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ o = {t e. (u LnOp w) | ((unormOpw)` t) < +oo})}

This definition is referenced by:  bloval 9781

Copyright terms: Public domain