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 28774
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 28695 . 2 class 0
2 chba 28690 . 2 class
31, 2wcel 2110 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  28793  hvaddid2  28794  hvmul0  28795  hv2neg  28799  hvsub0  28847  hi01  28867  hi02  28868  norm0  28899  normneg  28915  norm3difi  28918  hilablo  28931  hilid  28932  hlim0  29006  helch  29014  hsn0elch  29019  elch0  29025  hhssnv  29035  ocsh  29054  shscli  29088  choc0  29097  shintcli  29100  pj0i  29464  df0op2  29523  hon0  29564  ho01i  29599  nmopsetn0  29636  nmfnsetn0  29649  dmadjrnb  29677  nmopge0  29682  nmfnge0  29698  bra0  29721  lnop0  29737  lnopmul  29738  0cnop  29750  nmop0  29757  nmfn0  29758  nmop0h  29762  nmcexi  29797  nmcopexi  29798  lnfn0i  29813  lnfnmuli  29815  nmcfnexi  29822  nlelshi  29831  riesz3i  29833  hmopidmchi  29922
  Copyright terms: Public domain W3C validator