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 ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ 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 ∈ u LnOp w | u normOp OLD w ⁡ t < +∞
17 1 3 2 2 16 cmpo class u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ u LnOp w | u normOp OLD w ⁡ t < +∞
18 0 17 wceq wff BLnOp = u ∈ NrmCVec , w ∈ NrmCVec ⟼ t ∈ u LnOp w | u normOp OLD w ⁡ t < +∞