Theorem hoid1i

Description: Composition of Hilbert space operator with unit identity. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hoaddid1.1	⊢ 𝑇 : ℋ ⟶ ℋ
Assertion	hoid1i	⊢ ( 𝑇 ∘ Iop ) = 𝑇

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	⊢ 𝑇 : ℋ ⟶ ℋ
2		df-iop	⊢ Iop = ( projℎ ‘ ℋ )
3	2	coeq2i	⊢ ( 𝑇 ∘ Iop ) = ( 𝑇 ∘ ( projℎ ‘ ℋ ) )
4		helch	⊢ ℋ ∈ Cℋ
5	4	pjfi	⊢ ( projℎ ‘ ℋ ) : ℋ ⟶ ℋ
6	1 5	hocoi	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) ) )
7		pjch1	⊢ ( 𝑥 ∈ ℋ → ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) = 𝑥 )
8	7	fveq2d	⊢ ( 𝑥 ∈ ℋ → ( 𝑇 ‘ ( ( projℎ ‘ ℋ ) ‘ 𝑥 ) ) = ( 𝑇 ‘ 𝑥 ) )
9	6 8	eqtrd	⊢ ( 𝑥 ∈ ℋ → ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
10	9	rgen	⊢ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 )
11	1 5	hocofi	⊢ ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) : ℋ ⟶ ℋ
12	11 1	hoeqi	⊢ ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) ↔ ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) = 𝑇 )
13	10 12	mpbi	⊢ ( 𝑇 ∘ ( projℎ ‘ ℋ ) ) = 𝑇
14	3 13	eqtri	⊢ ( 𝑇 ∘ Iop ) = 𝑇