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	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ ( normop ‘ 𝑇 ) ∈ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		lnopcnbd	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ 𝑇 ∈ BndLinOp ) )
2		elbdop2	⊢ ( 𝑇 ∈ BndLinOp ↔ ( 𝑇 ∈ LinOp ∧ ( normop ‘ 𝑇 ) ∈ ℝ ) )
3	2	baib	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ BndLinOp ↔ ( normop ‘ 𝑇 ) ∈ ℝ ) )
4	1 3	bitrd	⊢ ( 𝑇 ∈ LinOp → ( 𝑇 ∈ ContOp ↔ ( normop ‘ 𝑇 ) ∈ ℝ ) )