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 ) |
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 ) |