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

Axiom ax-hv0cl 27244
Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hv0cl 0 ∈ ℋ

Detailed syntax breakdown of Axiom ax-hv0cl
StepHypRef Expression
1 c0v 27165 . 2 class 0
2 chil 27160 . 2 class
31, 2wcel 1977 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  27263  hvaddid2  27264  hvmul0  27265  hv2neg  27269  hvsub0  27317  hi01  27337  hi02  27338  norm0  27369  normneg  27385  norm3difi  27388  hilablo  27401  hilid  27402  hlim0  27476  helch  27484  hsn0elch  27489  elch0  27495  hhssnv  27505  ocsh  27526  shscli  27560  choc0  27569  shintcli  27572  pj0i  27936  df0op2  27995  hon0  28036  ho01i  28071  nmopsetn0  28108  nmfnsetn0  28121  dmadjrnb  28149  nmopge0  28154  nmfnge0  28170  bra0  28193  lnop0  28209  lnopmul  28210  0cnop  28222  nmop0  28229  nmfn0  28230  nmop0h  28234  nmcexi  28269  nmcopexi  28270  lnfn0i  28285  lnfnmuli  28287  nmcfnexi  28294  nlelshi  28303  riesz3i  28305  hmopidmchi  28394
  Copyright terms: Public domain W3C validator