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 )