Theorem hoico2

Description: Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoico2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( Iop ∘ 𝑇 ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		dfiop2	⊢ Iop = ( I ↾ ℋ )
2	1	coeq1i	⊢ ( Iop ∘ 𝑇 ) = ( ( I ↾ ℋ ) ∘ 𝑇 )
3		fcoi2	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ( I ↾ ℋ ) ∘ 𝑇 ) = 𝑇 )
4	2 3	eqtrid	⊢ ( 𝑇 : ℋ ⟶ ℋ → ( Iop ∘ 𝑇 ) = 𝑇 )