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 29774
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 29695 . 2 class 0
2 chba 29690 . 2 class
31, 2wcel 2106 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  29793  hvaddid2  29794  hvmul0  29795  hv2neg  29799  hvsub0  29847  hi01  29867  hi02  29868  norm0  29899  normneg  29915  norm3difi  29918  hilablo  29931  hilid  29932  hlim0  30006  helch  30014  hsn0elch  30019  elch0  30025  hhssnv  30035  ocsh  30054  shscli  30088  choc0  30097  shintcli  30100  pj0i  30464  df0op2  30523  hon0  30564  ho01i  30599  nmopsetn0  30636  nmfnsetn0  30649  dmadjrnb  30677  nmopge0  30682  nmfnge0  30698  bra0  30721  lnop0  30737  lnopmul  30738  0cnop  30750  nmop0  30757  nmfn0  30758  nmop0h  30762  nmcexi  30797  nmcopexi  30798  lnfn0i  30813  lnfnmuli  30815  nmcfnexi  30822  nlelshi  30831  riesz3i  30833  hmopidmchi  30922
  Copyright terms: Public domain W3C validator