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:\mathscr{H}⟶\mathscr{H}\to T\circ I_{\mathrm{op}}=T$$

Proof

Step	Hyp	Ref	Expression
1		dfiop2	$$⊢I_{\mathrm{op}}={\mathrm{I}\upharpoonright }_{\mathscr{H}}$$
2	1	coeq2i	$$⊢T\circ I_{\mathrm{op}}=T\circ \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)$$
3		fcoi1	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T\circ \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)=T$$
4	2 3	syl5eq	$$⊢T:\mathscr{H}⟶\mathscr{H}\to T\circ I_{\mathrm{op}}=T$$