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

Metamath Proof Explorer

Theorem lnfncnbd

Description: A linear functional is continuous iff it is bounded. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfncnbd 
|- ( T e. LinFn -> ( T e. ContFn <-> ( normfn ` T ) e. RR ) )

Proof

Step Hyp Ref Expression
1 nmcfnex 
 |-  ( ( T e. LinFn /\ T e. ContFn ) -> ( normfn ` T ) e. RR )
2 1 ex 
 |-  ( T e. LinFn -> ( T e. ContFn -> ( normfn ` T ) e. RR ) )
3 simpr 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> ( normfn ` T ) e. RR )
4 nmbdfnlb 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR /\ y e. ~H ) -> ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) )
5 4 3expa 
 |-  ( ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) /\ y e. ~H ) -> ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) )
6 5 ralrimiva 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> A. y e. ~H ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) )
7 oveq1 
 |-  ( x = ( normfn ` T ) -> ( x x. ( normh ` y ) ) = ( ( normfn ` T ) x. ( normh ` y ) ) )
8 7 breq2d 
 |-  ( x = ( normfn ` T ) -> ( ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) ) )
9 8 ralbidv 
 |-  ( x = ( normfn ` T ) -> ( A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> A. y e. ~H ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) ) )
10 9 rspcev 
 |-  ( ( ( normfn ` T ) e. RR /\ A. y e. ~H ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) ) -> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
11 3 6 10 syl2anc 
 |-  ( ( T e. LinFn /\ ( normfn ` T ) e. RR ) -> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )
12 11 ex 
 |-  ( T e. LinFn -> ( ( normfn ` T ) e. RR -> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
13 lnfncon 
 |-  ( T e. LinFn -> ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
14 12 13 sylibrd 
 |-  ( T e. LinFn -> ( ( normfn ` T ) e. RR -> T e. ContFn ) )
15 2 14 impbid 
 |-  ( T e. LinFn -> ( T e. ContFn <-> ( normfn ` T ) e. RR ) )