Metamath Proof Explorer

Theorem lnfn0

Description: The value of a linear Hilbert space functional at zero is zero. Remark in Beran p. 99. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfn0 
|- ( T e. LinFn -> ( T ` 0h ) = 0 )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( T ` 0h ) = ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` 0h ) )
2 1 eqeq1d 
 |-  ( T = if ( T e. LinFn , T , ( ~H X. { 0 } ) ) -> ( ( T ` 0h ) = 0 <-> ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` 0h ) = 0 ) )
3 0lnfn 
 |-  ( ~H X. { 0 } ) e. LinFn
4 3 elimel 
 |-  if ( T e. LinFn , T , ( ~H X. { 0 } ) ) e. LinFn
5 4 lnfn0i 
 |-  ( if ( T e. LinFn , T , ( ~H X. { 0 } ) ) ` 0h ) = 0
6 2 5 dedth 
 |-  ( T e. LinFn -> ( T ` 0h ) = 0 )