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

Metamath Proof Explorer

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	$⊢ 0_{hop} = {proj}_{ℎ} (0_{ℋ})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ch0o	$class 0_{hop}$
1		cpjh	$class {proj}_{ℎ}$
2		c0h	$class 0_{ℋ}$
3	2 1	cfv	$class {proj}_{ℎ} (0_{ℋ})$
4	0 3	wceq	$wff 0_{hop} = {proj}_{ℎ} (0_{ℋ})$