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 = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { 𝑡 ∈ ( 𝑢 LnOp 𝑤 ) ∣ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cblo	⊢ BLnOp
1		vu	⊢ 𝑢
2		cnv	⊢ NrmCVec
3		vw	⊢ 𝑤
4		vt	⊢ 𝑡
5	1	cv	⊢ 𝑢
6		clno	⊢ LnOp
7	3	cv	⊢ 𝑤
8	5 7 6	co	⊢ ( 𝑢 LnOp 𝑤 )
9		cnmoo	⊢ normOpOLD
10	5 7 9	co	⊢ ( 𝑢 normOpOLD 𝑤 )
11	4	cv	⊢ 𝑡
12	11 10	cfv	⊢ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 )
13		clt	⊢ <
14		cpnf	⊢ +∞
15	12 14 13	wbr	⊢ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞
16	15 4 8	crab	⊢ { 𝑡 ∈ ( 𝑢 LnOp 𝑤 ) ∣ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ }
17	1 3 2 2 16	cmpo	⊢ ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { 𝑡 ∈ ( 𝑢 LnOp 𝑤 ) ∣ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } )
18	0 17	wceq	⊢ BLnOp = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { 𝑡 ∈ ( 𝑢 LnOp 𝑤 ) ∣ ( ( 𝑢 normOpOLD 𝑤 ) ‘ 𝑡 ) < +∞ } )