Theorem ho0f

Description: Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	ho0f	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right):\mathscr{H}⟶\mathscr{H}$$
3		df-h0op	$$⊢0_{\mathrm{hop}}={\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right)$$
4	3	feq1i	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(0_{\mathscr{H}}\right):\mathscr{H}⟶\mathscr{H}$$
5	2 4	mpbir	$$⊢0_{\mathrm{hop}}:\mathscr{H}⟶\mathscr{H}$$