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

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 = ( 𝑢 ∈ 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 𝑤 ) ‘ 𝑡 ) < +∞ } )