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 e. LinOp -> ( T e. ContOp <-> ( normop ` T ) e. RR ) )

Proof

Step Hyp Ref Expression
1 lnopcnbd 
 |-  ( T e. LinOp -> ( T e. ContOp <-> T e. BndLinOp ) )
2 elbdop2 
 |-  ( T e. BndLinOp <-> ( T e. LinOp /\ ( normop ` T ) e. RR ) )
3 2 baib 
 |-  ( T e. LinOp -> ( T e. BndLinOp <-> ( normop ` T ) e. RR ) )
4 1 3 bitrd 
 |-  ( T e. LinOp -> ( T e. ContOp <-> ( normop ` T ) e. RR ) )