Metamath Proof Explorer

Theorem lnopf

Description: A linear Hilbert space operator is a Hilbert space operator. (Contributed by NM, 18-Jan-2006) (New usage is discouraged.)

Ref Expression
Assertion lnopf 
|- ( T e. LinOp -> T : ~H --> ~H )

Proof

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