Theorem 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 e. ( LinOp i^i ContOp ) <-> T e. BndLinOp )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( T e. ( LinOp i^i ContOp ) <-> ( T e. LinOp /\ T e. ContOp ) )
2		lnopcnbd	|- ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) )
3	2	biimpa	|- ( ( T e. LinOp /\ T e. ContOp ) -> T e. BndLinOp )
4		bdopln	|- ( T e. BndLinOp -> T e. LinOp )
5	2	biimparc	|- ( ( T e. BndLinOp /\ T e. LinOp ) -> T e. ContOp )
6	4 5	mpdan	|- ( T e. BndLinOp -> T e. ContOp )
7	4 6	jca	|- ( T e. BndLinOp -> ( T e. LinOp /\ T e. ContOp ) )
8	3 7	impbii	|- ( ( T e. LinOp /\ T e. ContOp ) <-> T e. BndLinOp )
9	1 8	bitri	|- ( T e. ( LinOp i^i ContOp ) <-> T e. BndLinOp )