Definition df-ch0

Description: Define the zero for closed subspaces of Hilbert space. See h0elch for closure law. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ch0	⊢ 0ℋ = { 0ℎ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c0h	⊢ 0ℋ
1		c0v	⊢ 0ℎ
2	1	csn	⊢ { 0ℎ }
3	0 2	wceq	⊢ 0ℋ = { 0ℎ }