Theorem lnopcnbd

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

	Ref	Expression
Assertion	lnopcnbd	|- ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) )

Proof

Step	Hyp	Ref	Expression
1		nmcopex	|- ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR )
2	1	ex	|- ( T e. LinOp -> ( T e. ContOp -> ( normop ` T ) e. RR ) )
3		elbdop2	|- ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )
4	3	baibr	|- ( T e. LinOp -> ( ( normop ` T ) e. RR <-> T e. BndLinOp ) )
5	2 4	sylibd	|- ( T e. LinOp -> ( T e. ContOp -> T e. BndLinOp ) )
6		nmopre	|- ( T e. BndLinOp -> ( normop ` T ) e. RR )
7		nmbdoplb	|- ( ( T e. BndLinOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
8	7	ralrimiva	|- ( T e. BndLinOp -> A. y e. ~H ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
9		oveq1	|- ( x = ( normop ` T ) -> ( x x. ( normh ` y ) ) = ( ( normop ` T ) x. ( normh ` y ) ) )
10	9	breq2d	|- ( x = ( normop ` T ) -> ( ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) )
11	10	ralbidv	|- ( x = ( normop ` T ) -> ( A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> A. y e. ~H ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) )
12	11	rspcev	|- ( ( ( normop ` T ) e. RR /\ A. y e. ~H ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) ) -> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
13	6 8 12	syl2anc	|- ( T e. BndLinOp -> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
14		lnopcon	|- ( T e. LinOp -> ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
15	13 14	imbitrrid	|- ( T e. LinOp -> ( T e. BndLinOp -> T e. ContOp ) )
16	5 15	impbid	|- ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) )