Theorem ho0f

Description: Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	ho0f	⊢ 0hop : ℋ ⟶ ℋ

Proof

Step	Hyp	Ref	Expression
1		h0elch	⊢ 0ℋ ∈ Cℋ
2	1	pjfi	⊢ ( projℎ ‘ 0ℋ ) : ℋ ⟶ ℋ
3		df-h0op	⊢ 0hop = ( projℎ ‘ 0ℋ )
4	3	feq1i	⊢ ( 0hop : ℋ ⟶ ℋ ↔ ( projℎ ‘ 0ℋ ) : ℋ ⟶ ℋ )
5	2 4	mpbir	⊢ 0hop : ℋ ⟶ ℋ