![]() |
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 31197. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-h0v | ⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c0v 30953 | . 2 class 0ℎ | |
2 | cva 30949 | . . . . 5 class +ℎ | |
3 | csm 30950 | . . . . 5 class ·ℎ | |
4 | 2, 3 | cop 4637 | . . . 4 class 〈 +ℎ , ·ℎ 〉 |
5 | cno 30952 | . . . 4 class normℎ | |
6 | 4, 5 | cop 4637 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 |
7 | cn0v 30617 | . . 3 class 0vec | |
8 | 6, 7 | cfv 6563 | . 2 class (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
9 | 1, 8 | wceq 1537 | 1 wff 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) |
Colors of variables: wff setvar class |
This definition is referenced by: axhv0cl-zf 31014 axhvaddid-zf 31015 axhvmul0-zf 31021 axhis4-zf 31026 |
Copyright terms: Public domain | W3C validator |