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	|- T : ~H --> ~H
Assertion	hoid1ri	|- ( Iop o. T ) = T

Proof

Step	Hyp	Ref	Expression
1		hoaddid1.1	|- T : ~H --> ~H
2		df-iop	|- Iop = ( projh ` ~H )
3	2	coeq1i	|- ( Iop o. T ) = ( ( projh ` ~H ) o. T )
4		helch	|- ~H e. CH
5	4	pjfi	|- ( projh ` ~H ) : ~H --> ~H
6	5 1	hocoi	|- ( x e. ~H -> ( ( ( projh ` ~H ) o. T ) ` x ) = ( ( projh ` ~H ) ` ( T ` x ) ) )
7	1	ffvelrni	|- ( x e. ~H -> ( T ` x ) e. ~H )
8		pjch1	|- ( ( T ` x ) e. ~H -> ( ( projh ` ~H ) ` ( T ` x ) ) = ( T ` x ) )
9	7 8	syl	|- ( x e. ~H -> ( ( projh ` ~H ) ` ( T ` x ) ) = ( T ` x ) )
10	6 9	eqtrd	|- ( x e. ~H -> ( ( ( projh ` ~H ) o. T ) ` x ) = ( T ` x ) )
11	10	rgen	|- A. x e. ~H ( ( ( projh ` ~H ) o. T ) ` x ) = ( T ` x )
12	5 1	hocofi	|- ( ( projh ` ~H ) o. T ) : ~H --> ~H
13	12 1	hoeqi	|- ( A. x e. ~H ( ( ( projh ` ~H ) o. T ) ` x ) = ( T ` x ) <-> ( ( projh ` ~H ) o. T ) = T )
14	11 13	mpbi	|- ( ( projh ` ~H ) o. T ) = T
15	3 14	eqtri	|- ( Iop o. T ) = T