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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ch0o	⊢ 0hop
1		cpjh	⊢ projℎ
2		c0h	⊢ 0ℋ
3	2 1	cfv	⊢ ( projℎ ‘ 0ℋ )
4	0 3	wceq	⊢ 0hop = ( projℎ ‘ 0ℋ )