Theorem hoico1

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

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

Proof

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