Metamath Proof Explorer

Theorem lnopcon

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) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( T = if ( T e. LinOp , T , ( _I |` ~H ) ) -> ( T e. ContOp <-> if ( T e. LinOp , T , ( _I |` ~H ) ) e. ContOp ) )
2 fveq1 
 |-  ( T = if ( T e. LinOp , T , ( _I |` ~H ) ) -> ( T ` y ) = ( if ( T e. LinOp , T , ( _I |` ~H ) ) ` y ) )
3 2 fveq2d 
 |-  ( T = if ( T e. LinOp , T , ( _I |` ~H ) ) -> ( normh ` ( T ` y ) ) = ( normh ` ( if ( T e. LinOp , T , ( _I |` ~H ) ) ` y ) ) )
4 3 breq1d 
 |-  ( T = if ( T e. LinOp , T , ( _I |` ~H ) ) -> ( ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( normh ` ( if ( T e. LinOp , T , ( _I |` ~H ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
5 4 rexralbidv 
 |-  ( T = if ( T e. LinOp , T , ( _I |` ~H ) ) -> ( E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> E. x e. RR A. y e. ~H ( normh ` ( if ( T e. LinOp , T , ( _I |` ~H ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
6 1 5 bibi12d 
 |-  ( T = if ( T e. LinOp , T , ( _I |` ~H ) ) -> ( ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) <-> ( if ( T e. LinOp , T , ( _I |` ~H ) ) e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( if ( T e. LinOp , T , ( _I |` ~H ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) ) ) )
7 idlnop 
 |-  ( _I |` ~H ) e. LinOp
8 7 elimel 
 |-  if ( T e. LinOp , T , ( _I |` ~H ) ) e. LinOp
9 8 lnopconi 
 |-  ( if ( T e. LinOp , T , ( _I |` ~H ) ) e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( if ( T e. LinOp , T , ( _I |` ~H ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) )
10 6 9 dedth 
 |-  ( T e. LinOp -> ( T e. ContOp <-> E. x e. RR A. y e. ~H ( normh ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )