Metamath Proof Explorer

Theorem hoico1

Description: Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

Ref Expression
Assertion hoico1 
|- ( T : ~H --> ~H -> ( T o. Iop ) = T )

Proof

Step Hyp Ref Expression
1 dfiop2 
 |-  Iop = ( _I |` ~H )
2 1 coeq2i 
 |-  ( T o. Iop ) = ( T o. ( _I |` ~H ) )
3 fcoi1 
 |-  ( T : ~H --> ~H -> ( T o. ( _I |` ~H ) ) = T )
4 2 3 syl5eq 
 |-  ( T : ~H --> ~H -> ( T o. Iop ) = T )