This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$class 0_{ℋ}$
1		c0v	$class 0_{ℎ}$
2	1	csn	$class \{0_{ℎ}\}$
3	0 2	wceq	$wff 0_{ℋ} = \{0_{ℎ}\}$