This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )