Theorem hoid1ri

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	hoid1ri	⊢ ( Iop ∘ 𝑇 ) = 𝑇

Proof

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