This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-bdop

Description: Define the set of bounded linear Hilbert space operators. (See df-hosum for definition of operator.) (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	df-bdop	$⊢ BndLinOp = \{t \in LinOp \| {norm}_{op} (t) < +∞\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbo	$class BndLinOp$
1		vt	$setvar t$
2		clo	$class LinOp$
3		cnop	$class {norm}_{op}$
4	1	cv	$setvar t$
5	4 3	cfv	$class {norm}_{op} (t)$
6		clt	$class <$
7		cpnf	$class +∞$
8	5 7 6	wbr	$wff {norm}_{op} (t) < +∞$
9	8 1 2	crab	$class \{t \in LinOp \| {norm}_{op} (t) < +∞\}$
10	0 9	wceq	$wff BndLinOp = \{t \in LinOp \| {norm}_{op} (t) < +∞\}$