Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-h0op | Structured version Visualization version Unicode version |
Description: Define the Hilbert space zero operator. See df0op2 28611 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0op |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ch0o 27800 | . 2 | |
2 | c0h 27792 | . . 3 | |
3 | cpjh 27794 | . . 3 | |
4 | 2, 3 | cfv 5888 | . 2 |
5 | 1, 4 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: ho0val 28609 ho0f 28610 pjbdlni 29008 |
Copyright terms: Public domain | W3C validator |