Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-h0v | Structured version Visualization version Unicode version |
Description: Define the zero vector of Hilbert space. Note that is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. It is proved from the axioms as theorem hh0v 28025. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 27781 | . 2 | |
2 | cva 27777 | . . . . 5 | |
3 | csm 27778 | . . . . 5 | |
4 | 2, 3 | cop 4183 | . . . 4 |
5 | cno 27780 | . . . 4 | |
6 | 4, 5 | cop 4183 | . . 3 |
7 | cn0v 27443 | . . 3 | |
8 | 6, 7 | cfv 5888 | . 2 |
9 | 1, 8 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: axhv0cl-zf 27842 axhvaddid-zf 27843 axhvmul0-zf 27849 axhis4-zf 27854 |
Copyright terms: Public domain | W3C validator |