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 31022
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 30943 . 2 class 0
2 chba 30938 . 2 class
31, 2wcel 2108 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  31041  hvaddlid  31042  hvmul0  31043  hv2neg  31047  hvsub0  31095  hi01  31115  hi02  31116  norm0  31147  normneg  31163  norm3difi  31166  hilablo  31179  hilid  31180  hlim0  31254  helch  31262  hsn0elch  31267  elch0  31273  hhssnv  31283  ocsh  31302  shscli  31336  choc0  31345  shintcli  31348  pj0i  31712  df0op2  31771  hon0  31812  ho01i  31847  nmopsetn0  31884  nmfnsetn0  31897  dmadjrnb  31925  nmopge0  31930  nmfnge0  31946  bra0  31969  lnop0  31985  lnopmul  31986  0cnop  31998  nmop0  32005  nmfn0  32006  nmop0h  32010  nmcexi  32045  nmcopexi  32046  lnfn0i  32061  lnfnmuli  32063  nmcfnexi  32070  nlelshi  32079  riesz3i  32081  hmopidmchi  32170
  Copyright terms: Public domain W3C validator