Metamath Proof Explorer

Theorem hoival

Description: The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoival 
|- ( A e. ~H -> ( Iop ` A ) = A )

Proof

Step Hyp Ref Expression
1 df-iop 
 |-  Iop = ( projh ` ~H )
2 1 fveq1i 
 |-  ( Iop ` A ) = ( ( projh ` ~H ) ` A )
3 pjch1 
 |-  ( A e. ~H -> ( ( projh ` ~H ) ` A ) = A )
4 2 3 syl5eq 
 |-  ( A e. ~H -> ( Iop ` A ) = A )