Metamath Proof Explorer

Theorem hmopf

Description: A Hermitian operator is a Hilbert space operator (mapping). (Contributed by NM, 19-Mar-2006) (New usage is discouraged.)

Ref Expression
Assertion hmopf 
|- ( T e. HrmOp -> T : ~H --> ~H )

Proof

Step Hyp Ref Expression
1 elhmop 
 |-  ( T e. HrmOp <-> ( T : ~H --> ~H /\ A. x e. ~H A. y e. ~H ( x .ih ( T ` y ) ) = ( ( T ` x ) .ih y ) ) )
2 1 simplbi 
 |-  ( T e. HrmOp -> T : ~H --> ~H )