![]() |
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 30152. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0v | ⊢ 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 29908 | . 2 class 0ℎ | |
2 | cva 29904 | . . . . 5 class +ℎ | |
3 | csm 29905 | . . . . 5 class ·ℎ | |
4 | 2, 3 | cop 4593 | . . . 4 class ⟨ +ℎ , ·ℎ ⟩ |
5 | cno 29907 | . . . 4 class normℎ | |
6 | 4, 5 | cop 4593 | . . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩ |
7 | cn0v 29572 | . . 3 class 0vec | |
8 | 6, 7 | cfv 6497 | . 2 class (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩) |
9 | 1, 8 | wceq 1542 | 1 wff 0ℎ = (0vec‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩) |
Colors of variables: wff setvar class |
This definition is referenced by: axhv0cl-zf 29969 axhvaddid-zf 29970 axhvmul0-zf 29976 axhis4-zf 29981 |
Copyright terms: Public domain | W3C validator |