Metamath Proof Explorer

Theorem hoico2

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

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

Proof

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