# Metamath Proof Explorer

## 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}}_{ℋ}$
pjcohocl.2 ${⊢}{T}:ℋ⟶ℋ$
Assertion pjcohocli ${⊢}{A}\in ℋ\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}}_{ℋ}$
2 pjcohocl.2 ${⊢}{T}:ℋ⟶ℋ$
3 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
4 3 2 hocoi ${⊢}{A}\in ℋ\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 ℋ\to {T}\left({A}\right)\in ℋ$
6 1 pjcli ${⊢}{T}\left({A}\right)\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({T}\left({A}\right)\right)\in {H}$
7 5 6 syl ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({T}\left({A}\right)\right)\in {H}$
8 4 7 eqeltrd ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {T}\right)\left({A}\right)\in {H}$