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

Metamath Proof Explorer

Theorem bdopln

Description: A bounded linear Hilbert space operator is a linear operator. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion bdopln ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )

Proof

Step Hyp Ref Expression
1 elbdop ⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) < +∞ ) )
2 1 simplbi ⊢ ( 𝑇 ∈ BndLinOp → 𝑇 ∈ LinOp )