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 = ( projℎ ‘ ℋ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chio	⊢ Iop
1		cpjh	⊢ projℎ
2		chba	⊢ ℋ
3	2 1	cfv	⊢ ( projℎ ‘ ℋ )
4	0 3	wceq	⊢ Iop = ( projℎ ‘ ℋ )