Metamath Proof Explorer

Theorem lnfncon

Description: A condition equivalent to " T is continuous" when T is linear. Theorem 3.5(iii) of Beran p. 99. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( T e. ContFn <-> if ( T e. LinFn , T , ( ~H X. { 0 } ) ) e. ContFn ) )
2 fveq1 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( T ` y ) = ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` y ) )
3 2 fveq2d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( abs ` ( T ` y ) ) = ( abs ` ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` y ) ) )
4 3 breq1d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> ( abs ` ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
5 4 rexralbidv 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) <-> E. x e. RR A. y e. ~H ( abs ` ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) ) )
6 1 5 bibi12d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) <-> ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) ) ) )
7 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
8 7 elimel 
 |-  if ( T e. LinFn , T , ( ~H X. { 0 } ) ) e. LinFn
9 8 lnfnconi 
 |-  ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` y ) ) <_ ( x x. ( normh ` y ) ) )
10 6 9 dedth 
 |-  ( T e. LinFn -> ( T e. ContFn <-> E. x e. RR A. y e. ~H ( abs ` ( T ` y ) ) <_ ( x x. ( normh ` y ) ) ) )