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

Metamath Proof Explorer

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