Theorem hoid1ri

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	hoid1ri	$$⊢I_{\mathrm{op}}\circ T=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	coeq1i	$$⊢I_{\mathrm{op}}\circ T={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T$$
4		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right):\mathscr{H}⟶\mathscr{H}$$
6	5 1	hocoi	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(T\left(x\right)\right)$$
7	1	ffvelcdmi	$$⊢x\in \mathscr{H}\to T\left(x\right)\in \mathscr{H}$$
8		pjch1	$$⊢T\left(x\right)\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(T\left(x\right)\right)=T\left(x\right)$$
9	7 8	syl	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(T\left(x\right)\right)=T\left(x\right)$$
10	6 9	eqtrd	$$⊢x\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T\right)\left(x\right)=T\left(x\right)$$
11	10	rgen	$$⊢\forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T\right)\left(x\right)=T\left(x\right)$$
12	5 1	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T\right):\mathscr{H}⟶\mathscr{H}$$
13	12 1	hoeqi	$$⊢\forall x\in \mathscr{H}\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T\right)\left(x\right)=T\left(x\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T=T$$
14	11 13	mpbi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ T=T$$
15	3 14	eqtri	$$⊢I_{\mathrm{op}}\circ T=T$$