Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-h0v | Structured version Visualization version GIF version |
Description: Define the zero vector of Hilbert space. Note that 0vec 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 27409. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0v | ⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 27165 | . 2 class 0ℎ | |
2 | cva 27161 | . . . . 5 class +ℎ | |
3 | csm 27162 | . . . . 5 class ·ℎ | |
4 | 2, 3 | cop 4131 | . . . 4 class 〈 +ℎ , ·ℎ 〉 |
5 | cno 27164 | . . . 4 class normℎ | |
6 | 4, 5 | cop 4131 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
7 | cn0v 26827 | . . 3 class 0vec | |
8 | 6, 7 | cfv 5804 | . 2 class (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
9 | 1, 8 | wceq 1475 | 1 wff 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Colors of variables: wff setvar class |
This definition is referenced by: axhv0cl-zf 27226 axhvaddid-zf 27227 axhvmul0-zf 27233 axhis4-zf 27238 |
Copyright terms: Public domain | W3C validator |