Theorem dfiop2

Description: Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	dfiop2	|- Iop = ( _I |` ~H )

Proof

Step	Hyp	Ref	Expression
1		df-iop	|- Iop = ( projh ` ~H )
2		helch	|- ~H e. CH
3	2	pjfni	|- ( projh ` ~H ) Fn ~H
4		fnresi	|- ( _I |` ~H ) Fn ~H
5		pjch1	|- ( x e. ~H -> ( ( projh ` ~H ) ` x ) = x )
6		fvresi	|- ( x e. ~H -> ( ( _I |` ~H ) ` x ) = x )
7	5 6	eqtr4d	|- ( x e. ~H -> ( ( projh ` ~H ) ` x ) = ( ( _I |` ~H ) ` x ) )
8	7	rgen	|- A. x e. ~H ( ( projh ` ~H ) ` x ) = ( ( _I |` ~H ) ` x )
9		eqfnfv	|- ( ( ( projh ` ~H ) Fn ~H /\ ( _I |` ~H ) Fn ~H ) -> ( ( projh ` ~H ) = ( _I |` ~H ) <-> A. x e. ~H ( ( projh ` ~H ) ` x ) = ( ( _I |` ~H ) ` x ) ) )
10	8 9	mpbiri	|- ( ( ( projh ` ~H ) Fn ~H /\ ( _I |` ~H ) Fn ~H ) -> ( projh ` ~H ) = ( _I |` ~H ) )
11	3 4 10	mp2an	|- ( projh ` ~H ) = ( _I |` ~H )
12	1 11	eqtri	|- Iop = ( _I |` ~H )