Definition df-bdop 9725

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

Assertion

Ref	Expression
df-bdop	⊢ BndLinOp = (LinOp ∩ {t∣(t: ℋ –→ ℋ ⋀ (normop ‘t) < +∞)})

Detailed syntax breakdown of Definition df-bdop

Step	Hyp	Ref	Expression
1		cbo 8772	. 2 class BndLinOp
2		clo 8771	. . 3 class LinOp
3		chil 8743	. . . . . 6 class ℋ
4		vt	. . . . . . 7 set t
5	4	cv 954	. . . . . 6 class t
6	3, 3, 5	wf 3174	. . . . 5 wff t: ℋ –→ ℋ
7		cnop 8769	. . . . . . 7 class normop
8	5, 7	cfv 3178	. . . . . 6 class (normop ‘t)
9		cpnf 5466	. . . . . 6 class +∞
10		clt 5469	. . . . . 6 class <
11	8, 9, 10	wbr 2615	. . . . 5 wff (normop ‘t) < +∞
12	6, 11	wa 223	. . . 4 wff (t: ℋ –→ ℋ ⋀ (normop ‘t) < +∞)
13	12, 4	cab 1462	. . 3 class {t∣(t: ℋ –→ ℋ ⋀ (normop ‘t) < +∞)}
14	2, 13	cin 2043	. 2 class (LinOp ∩ {t∣(t: ℋ –→ ℋ ⋀ (normop ‘t) < +∞)})
15	1, 14	wceq 955	1 wff BndLinOp = (LinOp ∩ {t∣(t: ℋ –→ ℋ ⋀ (normop ‘t) < +∞)})

This definition is referenced by:  dfbdop2 9743

Copyright terms: Public domain