Metamath Proof Explorer

Definition df-blo

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

		Ref	Expression
	Assertion	df-blo	$⊢ BLnOp = (u \in NrmCVec, w \in NrmCVec ⟼ \{t \in (u LnOp w) \| (u {normOp}_{OLD} w) (t) < +∞\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cblo	$class BLnOp$
1		vu	$setvar u$
2		cnv	$class NrmCVec$
3		vw	$setvar w$
4		vt	$setvar t$
5	1	cv	$setvar u$
6		clno	$class LnOp$
7	3	cv	$setvar w$
8	5 7 6	co	$class (u LnOp w)$
9		cnmoo	$class {normOp}_{OLD}$
10	5 7 9	co	$class (u {normOp}_{OLD} w)$
11	4	cv	$setvar t$
12	11 10	cfv	$class (u {normOp}_{OLD} w) (t)$
13		clt	$class <$
14		cpnf	$class +∞$
15	12 14 13	wbr	$wff (u {normOp}_{OLD} w) (t) < +∞$
16	15 4 8	crab	$class \{t \in (u LnOp w) \| (u {normOp}_{OLD} w) (t) < +∞\}$
17	1 3 2 2 16	cmpo	$class (u \in NrmCVec, w \in NrmCVec ⟼ \{t \in (u LnOp w) \| (u {normOp}_{OLD} w) (t) < +∞\})$
18	0 17	wceq	$wff BLnOp = (u \in NrmCVec, w \in NrmCVec ⟼ \{t \in (u LnOp w) \| (u {normOp}_{OLD} w) (t) < +∞\})$