Theorem pjcohocli

Description: Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjcohocl.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjcohocl.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
Assertion	pjcohocli	$$⊢A\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ T\right)\left(A\right)\in H$$

Proof

Step	Hyp	Ref	Expression
1		pjcohocl.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjcohocl.2	$$⊢T:\mathscr{H}⟶\mathscr{H}$$
3	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
4	3 2	hocoi	$$⊢A\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ T\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(T\left(A\right)\right)$$
5	2	ffvelrni	$$⊢A\in \mathscr{H}\to T\left(A\right)\in \mathscr{H}$$
6	1	pjcli	$$⊢T\left(A\right)\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(T\left(A\right)\right)\in H$$
7	5 6	syl	$$⊢A\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(T\left(A\right)\right)\in H$$
8	4 7	eqeltrd	$$⊢A\in \mathscr{H}\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\circ T\right)\left(A\right)\in H$$