Definition df-bdop 11197

Description: Define the set of bounded linear Hilbert space operators. (See df-hosum 10931 for definition of operator.)

Assertion

Ref	Expression
df-bdop	|- BndLinOp = (LinOp i^i {t | (t:~H-->~H /\ (normop` t) < +oo)})

Detailed syntax breakdown of Definition df-bdop

Step	Hyp	Ref	Expression
1		cbo 10241	. 2 class BndLinOp
2		clo 10240	. . 3 class LinOp
3		chil 10212	. . . . . 6 class ~H
4		vt	. . . . . . 7 set t
5	4	cv 1135	. . . . . 6 class t
6	3, 3, 5	wf 3805	. . . . 5 wff t:~H-->~H
7		cnop 10238	. . . . . . 7 class normop
8	5, 7	cfv 3809	. . . . . 6 class (normop` t)
9		cpnf 6446	. . . . . 6 class +oo
10		clt 6449	. . . . . 6 class <
11	8, 9, 10	wbr 3158	. . . . 5 wff (normop` t) < +oo
12	6, 11	wa 239	. . . 4 wff (t:~H-->~H /\ (normop` t) < +oo)
13	12, 4	cab 1708	. . 3 class {t | (t:~H-->~H /\ (normop` t) < +oo)}
14	2, 13	cin 2425	. 2 class (LinOp i^i {t | (t:~H-->~H /\ (normop` t) < +oo)})
15	1, 14	wceq 1136	1 wff BndLinOp = (LinOp i^i {t | (t:~H-->~H /\ (normop` t) < +oo)})

This definition is referenced by:  dfbdop2 11215

Copyright terms: Public domain