Metamath Proof Explorer

Theorem lnopcnre

Description: A linear operator is continuous iff it is bounded. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopcnre ⊢ T ∈ LinOp → T ∈ ContOp ↔ norm op ⁡ T ∈ ℝ

Proof

Step Hyp Ref Expression
1 lnopcnbd ⊢ T ∈ LinOp → T ∈ ContOp ↔ T ∈ BndLinOp
2 elbdop2 ⊢ T ∈ BndLinOp ↔ T ∈ LinOp ∧ norm op ⁡ T ∈ ℝ
3 2 baib ⊢ T ∈ LinOp → T ∈ BndLinOp ↔ norm op ⁡ T ∈ ℝ
4 1 3 bitrd ⊢ T ∈ LinOp → T ∈ ContOp ↔ norm op ⁡ T ∈ ℝ