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

Metamath Proof Explorer

Definition df-bdop

Description: Define the set of bounded linear Hilbert space operators. (See df-hosum for definition of operator.) (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion df-bdop BndLinOp = { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbo ⊢ BndLinOp
1 vt ⊢ 𝑡
2 clo ⊢ LinOp
3 cnop ⊢ normop
4 1 cv ⊢ 𝑡
5 4 3 cfv ⊢ ( normop ‘ 𝑡 )
6 clt ⊢ <
7 cpnf ⊢ +∞
8 5 7 6 wbr ⊢ ( normop ‘ 𝑡 ) < +∞
9 8 1 2 crab ⊢ { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }
10 0 9 wceq ⊢ BndLinOp = { 𝑡 ∈ LinOp ∣ ( normop ‘ 𝑡 ) < +∞ }