Theorem hoid1i

Description: Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hoaddrid.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	hoid1i	$$⊢T\circ I_{\mathrm{op}}=T$$

Proof

Step	Hyp	Ref	Expression
1		hoaddrid.1	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
2		df-iop	$$⊢I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
3	2	coeq2i	$$⊢T\circ I_{\mathrm{op}}=T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
4		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right):\mathscr{H}⟶\mathscr{H}$$
6	1 5	hocoi	$$⊢x\in \mathscr{H}\to \left(T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right)\left(x\right)=T\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)\right)$$
7		pjch1	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)=x$$
8	7	fveq2d	$$⊢x\in \mathscr{H}\to T\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)\right)=T\left(x\right)$$
9	6 8	eqtrd	$$⊢x\in \mathscr{H}\to \left(T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right)\left(x\right)=T\left(x\right)$$
10	9	rgen	$$⊢\forall x\in \mathscr{H}\left(T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right)\left(x\right)=T\left(x\right)$$
11	1 5	hocofi	$$⊢\left(T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right):\mathscr{H}⟶\mathscr{H}$$
12	11 1	hoeqi	$$⊢\forall x\in \mathscr{H}\left(T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right)\left(x\right)=T\left(x\right)\leftrightarrow T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)=T$$
13	10 12	mpbi	$$⊢T\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)=T$$
14	3 13	eqtri	$$⊢T\circ I_{\mathrm{op}}=T$$