This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 : ℋ ⟶ ℋ |