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 ) )