lncnopbd

Description: A continuous linear operator is a bounded linear operator. This theorem justifies our use of "bounded linear" as an interchangeable condition for "continuous linear" used in some textbook proofs. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	lncnopbd	$⊢ T \in (LinOp \cap ContOp) \leftrightarrow T \in BndLinOp$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ T \in (LinOp \cap ContOp) \leftrightarrow (T \in LinOp \land T \in ContOp)$
2		lnopcnbd	$⊢ T \in LinOp \to (T \in ContOp \leftrightarrow T \in BndLinOp)$
3	2	biimpa	$⊢ (T \in LinOp \land T \in ContOp) \to T \in BndLinOp$
4		bdopln	$⊢ T \in BndLinOp \to T \in LinOp$
5	2	biimparc	$⊢ (T \in BndLinOp \land T \in LinOp) \to T \in ContOp$
6	4 5	mpdan	$⊢ T \in BndLinOp \to T \in ContOp$
7	4 6	jca	$⊢ T \in BndLinOp \to (T \in LinOp \land T \in ContOp)$
8	3 7	impbii	$⊢ (T \in LinOp \land T \in ContOp) \leftrightarrow T \in BndLinOp$
9	1 8	bitri	$⊢ T \in (LinOp \cap ContOp) \leftrightarrow T \in BndLinOp$

Metamath Proof Explorer

Theorem lncnopbd

Proof