HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-h0v Structured version   Visualization version   GIF version

Definition df-h0v 30990
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.)
Assertion
Ref Expression
df-h0v 0 = (0vec‘⟨⟨ + , · ⟩, norm⟩)

Detailed syntax breakdown of Definition df-h0v
StepHypRef Expression
1 c0v 30944 . 2 class 0
2 cva 30940 . . . . 5 class +
3 csm 30941 . . . . 5 class ·
42, 3cop 4631 . . . 4 class ⟨ + , ·
5 cno 30943 . . . 4 class norm
64, 5cop 4631 . . 3 class ⟨⟨ + , · ⟩, norm
7 cn0v 30608 . . 3 class 0vec
86, 7cfv 6560 . 2 class (0vec‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 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