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

Metamath Proof Explorer

Theorem ho0val

Description: Value of the zero Hilbert space operator (null projector). Remark in Beran p. 111. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	ho0val	$⊢ A \in ℋ \to 0_{hop} (A) = 0_{ℎ}$

Proof

Step	Hyp	Ref	Expression
1		choc1	$⊢ ⊥ (ℋ) = 0_{ℋ}$
2	1	fveq2i	$⊢ {proj}_{ℎ} (⊥ (ℋ)) = {proj}_{ℎ} (0_{ℋ})$
3		df-h0op	$⊢ 0_{hop} = {proj}_{ℎ} (0_{ℋ})$
4	2 3	eqtr4i	$⊢ {proj}_{ℎ} (⊥ (ℋ)) = 0_{hop}$
5	4	fveq1i	$⊢ {proj}_{ℎ} (⊥ (ℋ)) (A) = 0_{hop} (A)$
6		helch	$⊢ ℋ \in C_{ℋ}$
7		pjo	$⊢ (ℋ \in C_{ℋ} \land A \in ℋ) \to {proj}_{ℎ} (⊥ (ℋ)) (A) = {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (ℋ) (A)$
8	6 7	mpan	$⊢ A \in ℋ \to {proj}_{ℎ} (⊥ (ℋ)) (A) = {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (ℋ) (A)$
9	5 8	eqtr3id	$⊢ A \in ℋ \to 0_{hop} (A) = {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (ℋ) (A)$
10	6	pjhcli	$⊢ A \in ℋ \to {proj}_{ℎ} (ℋ) (A) \in ℋ$
11		hvsubid	$⊢ {proj}_{ℎ} (ℋ) (A) \in ℋ \to {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (ℋ) (A) = 0_{ℎ}$
12	10 11	syl	$⊢ A \in ℋ \to {proj}_{ℎ} (ℋ) (A) -_{ℎ} {proj}_{ℎ} (ℋ) (A) = 0_{ℎ}$
13	9 12	eqtrd	$⊢ A \in ℋ \to 0_{hop} (A) = 0_{ℎ}$