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 \in LinOp \to (T \in ContOp \leftrightarrow {norm}_{op} (T) \in ℝ)$

Step	Hyp	Ref	Expression
1		lnopcnbd	$⊢ T \in LinOp \to (T \in ContOp \leftrightarrow T \in BndLinOp)$
2		elbdop2	$⊢ T \in BndLinOp \leftrightarrow (T \in LinOp \land {norm}_{op} (T) \in ℝ)$
3	2	baib	$⊢ T \in LinOp \to (T \in BndLinOp \leftrightarrow {norm}_{op} (T) \in ℝ)$
4	1 3	bitrd	$⊢ T \in LinOp \to (T \in ContOp \leftrightarrow {norm}_{op} (T) \in ℝ)$