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

Metamath Proof Explorer

Theorem lnopconi

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

Ref Expression
Hypothesis lnopcon.1 
|- T e. LinOp
Assertion lnopconi 
|- ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )

Proof

Step Hyp Ref Expression
1 lnopcon.1 
 |-  T e. LinOp
2 nmcopex 
 |-  ( ( T e. LinOp /\ T e. ContOp ) -> ( normop ` T ) e. RR )
3 1 2 mpan 
 |-  ( T e. ContOp -> ( normop ` T ) e. RR )
4 nmcoplb 
 |-  ( ( T e. LinOp /\ T e. ContOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
5 1 4 mp3an1 
 |-  ( ( T e. ContOp /\ y e. ~H ) -> ( normh ` ( T ` y ) ) <_ ( ( normop ` T ) x. ( normh ` y ) ) )
6 1 lnopfi 
 |-  T : ~H --> ~H
7 elcnop 
 |-  ( T e. ContOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < z ) ) )
8 6 7 mpbiran 
 |-  ( T e. ContOp <-> A. x e. ~H A. z e. RR+ E. y e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < z ) )
9 6 ffvelcdmi 
 |-  ( y e. ~H -> ( T ` y ) e. ~H )
10 normcl 
 |-  ( ( T ` y ) e. ~H -> ( normh ` ( T ` y ) ) e. RR )
11 9 10 syl 
 |-  ( y e. ~H -> ( normh ` ( T ` y ) ) e. RR )
12 1 lnopsubi 
 |-  ( ( w e. ~H /\ x e. ~H ) -> ( T ` ( w -h x ) ) = ( ( T ` w ) -h ( T ` x ) ) )
13 3 5 8 11 12 lnconi 
 |-  ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) )