|   | 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 31188. (Contributed by NM, 31-May-2008.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| df-h0v | ⊢ 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | c0v 30944 | . 2 class 0ℎ | |
| 2 | cva 30940 | . . . . 5 class +ℎ | |
| 3 | csm 30941 | . . . . 5 class ·ℎ | |
| 4 | 2, 3 | cop 4631 | . . . 4 class 〈 +ℎ , ·ℎ 〉 | 
| 5 | cno 30943 | . . . 4 class normℎ | |
| 6 | 4, 5 | cop 4631 | . . 3 class 〈〈 +ℎ , ·ℎ 〉, normℎ〉 | 
| 7 | cn0v 30608 | . . 3 class 0vec | |
| 8 | 6, 7 | cfv 6560 | . 2 class (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | 
| 9 | 1, 8 | wceq 1539 | 1 wff 0ℎ = (0vec‘〈〈 +ℎ , ·ℎ 〉, normℎ〉) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: axhv0cl-zf 31005 axhvaddid-zf 31006 axhvmul0-zf 31012 axhis4-zf 31017 | 
| Copyright terms: Public domain | W3C validator |