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

Proof

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