Definition df-iop

Description: Define the Hilbert space identity operator. See dfiop2 for alternate definition. (Contributed by NM, 15-Nov-2000) (New usage is discouraged.)

	Ref	Expression
Assertion	df-iop	|- Iop = ( projh ` ~H )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chio	|- Iop
1		cpjh	|- projh
2		chba	|- ~H
3	2 1	cfv	|- ( projh ` ~H )
4	0 3	wceq	|- Iop = ( projh ` ~H )