Metamath Proof Explorer

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 : ~H --> ~H

Proof

Step Hyp Ref Expression
1 h0elch 
 |-  0H e. CH
2 1 pjfi 
 |-  ( projh ` 0H ) : ~H --> ~H
3 df-h0op 
 |-  0hop = ( projh ` 0H )
4 3 feq1i 
 |-  ( 0hop : ~H --> ~H <-> ( projh ` 0H ) : ~H --> ~H )
5 2 4 mpbir 
 |-  0hop : ~H --> ~H