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

Detailed syntax breakdown of Definition df-h0v
StepHypRef Expression
1 c0v 29908 . 2 class 0
2 cva 29904 . . . . 5 class +
3 csm 29905 . . . . 5 class ·
42, 3cop 4593 . . . 4 class ⟨ + , ·
5 cno 29907 . . . 4 class norm
64, 5cop 4593 . . 3 class ⟨⟨ + , · ⟩, norm
7 cn0v 29572 . . 3 class 0vec
86, 7cfv 6497 . 2 class (0vec‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 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