Definition df-iop 29528

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

Assertion

Ref	Expression
df-iop	⊢ Iop = (projℎ‘ ℋ)

Detailed syntax breakdown of Definition df-iop

Step	Hyp	Ref	Expression
1		chio 28723	. 2 class Iop
2		chba 28698	. . 3 class ℋ
3		cpjh 28716	. . 3 class projℎ
4	2, 3	cfv 6357	. 2 class (projℎ‘ ℋ)
5	1, 4	wceq 1537	1 wff Iop = (projℎ‘ ℋ)

This definition is referenced by:  dfiop2  29532  hoival  29534  hoid1i  29568  hoid1ri  29569  pjclem1  29974  pjclem3  29976  pjci  29979