Definition df-h0op

Description: Define the Hilbert space zero operator. See df0op2 for alternate definition. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-h0op	$$⊢0_{\mathrm{hop}}={\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)$$

Detailed syntax breakdown

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