Metamath Proof Explorer

Theorem lnopfi

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

Ref Expression
Hypothesis lnopl.1 
|- T e. LinOp
Assertion lnopfi 
|- T : ~H --> ~H

Proof

Step Hyp Ref Expression
1 lnopl.1 
 |-  T e. LinOp
2 lnopf 
 |-  ( T e. LinOp -> T : ~H --> ~H )
3 1 2 ax-mp 
 |-  T : ~H --> ~H