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 28872. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0v | ⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 28628 | . 2 class 0ℎ | |
2 | cva 28624 | . . . . 5 class +ℎ | |
3 | csm 28625 | . . . . 5 class ·ℎ | |
4 | 2, 3 | cop 4563 | . . . 4 class 〈 +ℎ , ·ℎ 〉 |
5 | cno 28627 | . . . 4 class normℎ | |
6 | 4, 5 | cop 4563 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
7 | cn0v 28292 | . . 3 class 0vec | |
8 | 6, 7 | cfv 6348 | . 2 class (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
9 | 1, 8 | wceq 1528 | 1 wff 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Colors of variables: wff setvar class |
This definition is referenced by: axhv0cl-zf 28689 axhvaddid-zf 28690 axhvmul0-zf 28696 axhis4-zf 28701 |
Copyright terms: Public domain | W3C validator |