Definition df-blo 29987

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

Assertion

Ref	Expression
df-blo	⊢ BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})

Distinct variable group:   𝑢,𝑡,𝑤

Detailed syntax breakdown of Definition df-blo

Step	Hyp	Ref	Expression
1		cblo 29983	. 2 class BLnOp
2		vu	. . 3 setvar 𝑢
3		vw	. . 3 setvar 𝑤
4		cnv 29825	. . 3 class NrmCVec
5		vt	. . . . . . 7 setvar 𝑡
6	5	cv 1541	. . . . . 6 class 𝑡
7	2	cv 1541	. . . . . . 7 class 𝑢
8	3	cv 1541	. . . . . . 7 class 𝑤
9		cnmoo 29982	. . . . . . 7 class normOpOLD
10	7, 8, 9	co 7406	. . . . . 6 class (𝑢 normOpOLD 𝑤)
11	6, 10	cfv 6541	. . . . 5 class ((𝑢 normOpOLD 𝑤)‘𝑡)
12		cpnf 11242	. . . . 5 class +∞
13		clt 11245	. . . . 5 class <
14	11, 12, 13	wbr 5148	. . . 4 wff ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞
15		clno 29981	. . . . 5 class LnOp
16	7, 8, 15	co 7406	. . . 4 class (𝑢 LnOp 𝑤)
17	14, 5, 16	crab 3433	. . 3 class {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞}
18	2, 3, 4, 4, 17	cmpo 7408	. 2 class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})
19	1, 18	wceq 1542	1 wff BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞})

This definition is referenced by:  bloval  30022