Theorem lnfnconi

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (Proof shortened by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	lnfncon.1	|- T e. LinFn
Assertion	lnfnconi	|- ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )

Proof

Step	Hyp	Ref	Expression
1		lnfncon.1	|- T e. LinFn
2		nmcfnex	|- ( ( T e. LinFn /\ T e. ContFn ) -> ( normfn ` T ) e. RR )
3	1 2	mpan	|- ( T e. ContFn -> ( normfn ` T ) e. RR )
4		nmcfnlb	|- ( ( T e. LinFn /\ T e. ContFn /\ y e. ~H ) -> ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) )
5	1 4	mp3an1	|- ( ( T e. ContFn /\ y e. ~H ) -> ( abs ` ( T ` y ) ) <_ ( ( normfn ` T ) x. ( normh ` y ) ) )
6	1	lnfnfi	|- T : ~H --> CC
7		elcnfn	|- ( T e. ContFn <-> ( T : ~H --> CC /\ A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < z ) ) )
8	6 7	mpbiran	|- ( T e. ContFn <-> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( abs ` ( ( T ` w ) - ( T ` x ) ) ) < z ) )
9	6	ffvelrni	|- ( y e. ~H -> ( T ` y ) e. CC )
10	9	abscld	|- ( y e. ~H -> ( abs ` ( T ` y ) ) e. RR )
11	1	lnfnsubi	|- ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) - ( T ` x ) ) )
12	3 5 8 10 11	lnconi	|- ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )