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 28708
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 28629 . 2 class 0
2 chba 28624 . 2 class
31, 2wcel 2105 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  28727  hvaddid2  28728  hvmul0  28729  hv2neg  28733  hvsub0  28781  hi01  28801  hi02  28802  norm0  28833  normneg  28849  norm3difi  28852  hilablo  28865  hilid  28866  hlim0  28940  helch  28948  hsn0elch  28953  elch0  28959  hhssnv  28969  ocsh  28988  shscli  29022  choc0  29031  shintcli  29034  pj0i  29398  df0op2  29457  hon0  29498  ho01i  29533  nmopsetn0  29570  nmfnsetn0  29583  dmadjrnb  29611  nmopge0  29616  nmfnge0  29632  bra0  29655  lnop0  29671  lnopmul  29672  0cnop  29684  nmop0  29691  nmfn0  29692  nmop0h  29696  nmcexi  29731  nmcopexi  29732  lnfn0i  29747  lnfnmuli  29749  nmcfnexi  29756  nlelshi  29765  riesz3i  29767  hmopidmchi  29856
  Copyright terms: Public domain W3C validator