Definition df-ch0 5157

Description: Define the zero for closed subspaces of Hilbert space. See h0elch 5159 for closure law.

Assertion

Ref	Expression
df-ch0	⊢ 0ℋ = {0v}

Detailed syntax breakdown of Definition df-ch0

Step	Hyp	Ref	Expression
1		c0h 4974	. 2 class 0ℋ
2		c0v 4961	. . 3 class 0v
3	2	csn 1808	. 2 class {0v}
4	1, 3	wceq 1091	1 wff 0ℋ = {0v}

This definition is referenced by:  elch0 5158  h0elch 5159  sh0let 5365  ho0 5612

metamath.org