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	⊢ 𝐻 ∈ Cℋ
	pjcohocl.2	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	pjcohocli	⊢ ( 𝐴 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝐴 ) ∈ 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		pjcohocl.1	⊢ 𝐻 ∈ Cℋ
2		pjcohocl.2	⊢ 𝑇 : ℋ ⟶ ℋ
3	1	pjfi	⊢ ( projℎ ‘ 𝐻 ) : ℋ ⟶ ℋ
4	3 2	hocoi	⊢ ( 𝐴 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝐴 ) = ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝐴 ) ) )
5	2	ffvelcdmi	⊢ ( 𝐴 ∈ ℋ → ( 𝑇 ‘ 𝐴 ) ∈ ℋ )
6	1	pjcli	⊢ ( ( 𝑇 ‘ 𝐴 ) ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ 𝐻 )
7	5 6	syl	⊢ ( 𝐴 ∈ ℋ → ( ( projℎ ‘ 𝐻 ) ‘ ( 𝑇 ‘ 𝐴 ) ) ∈ 𝐻 )
8	4 7	eqeltrd	⊢ ( 𝐴 ∈ ℋ → ( ( ( projℎ ‘ 𝐻 ) ∘ 𝑇 ) ‘ 𝐴 ) ∈ 𝐻 )