Metamath Proof Explorer
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 |
|- 0hop = ( projh ` 0H ) |
Detailed syntax breakdown
| Step |
Hyp |
Ref |
Expression |
| 0 |
|
ch0o |
|- 0hop |
| 1 |
|
cpjh |
|- projh |
| 2 |
|
c0h |
|- 0H |
| 3 |
2 1
|
cfv |
|- ( projh ` 0H ) |
| 4 |
0 3
|
wceq |
|- 0hop = ( projh ` 0H ) |