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	$$⊢I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chio	$$class{I}_{\mathrm{op}}$$
1		cpjh	$$class{\mathrm{proj}}_{ℎ}$$
2		chba	$$class\mathscr{H}$$
3	2 1	cfv	$$class{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
4	0 3	wceq	$$wff{I}_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$