Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-h0op | Structured version Visualization version GIF version |
Description: Define the Hilbert space zero operator. See df0op2 29833 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0op | ⊢ 0hop = (projℎ‘0ℋ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ch0o 29024 | . 2 class 0hop | |
2 | c0h 29016 | . . 3 class 0ℋ | |
3 | cpjh 29018 | . . 3 class projℎ | |
4 | 2, 3 | cfv 6380 | . 2 class (projℎ‘0ℋ) |
5 | 1, 4 | wceq 1543 | 1 wff 0hop = (projℎ‘0ℋ) |
Colors of variables: wff setvar class |
This definition is referenced by: ho0val 29831 ho0f 29832 pjbdlni 30230 |
Copyright terms: Public domain | W3C validator |