Metamath Proof Explorer

Theorem lnfnf

Description: A linear Hilbert space functional is a functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion lnfnf 
|- ( T e. LinFn -> T : ~H --> CC )

Proof

Step Hyp Ref Expression
1 ellnfn 
 |-  ( T e. LinFn <-> ( T : ~H --> CC /\ A. x e. CC A. y e. ~H A. z e. ~H ( T ` ( ( x .h y ) +h z ) ) = ( ( x x. ( T ` y ) ) + ( T ` z ) ) ) )
2 1 simplbi 
 |-  ( T e. LinFn -> T : ~H --> CC )