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 C
pjcohocl.2 T :
Assertion pjcohocli A proj H T A H


Step Hyp Ref Expression
1 pjcohocl.1 H C
2 pjcohocl.2 T :
3 1 pjfi proj H :
4 3 2 hocoi A proj H T A = proj H T A
5 2 ffvelrni A T A
6 1 pjcli T A proj H T A H
7 5 6 syl A proj H T A H
8 4 7 eqeltrd A proj H T A H