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

Axiom ax-hv0cl 22507
Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hv0cl  |-  0h  e.  ~H

Detailed syntax breakdown of Axiom ax-hv0cl
StepHypRef Expression
1 c0v 22428 . 2  class  0h
2 chil 22423 . 2  class  ~H
31, 2wcel 1726 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22526  hvmul0  22527  hv2neg  22531  hvsubsub4  22563  hvnegdi  22570  hvsubeq0  22571  hvaddcan  22573  hvsub0  22579  hvsubadd  22580  hi01  22599  hi02  22600  normlem9at  22624  norm0  22631  normsq  22637  normsub0  22639  norm-ii  22641  norm-iii  22643  normsub  22646  normneg  22647  normpyth  22648  norm3difi  22650  norm3dif  22653  norm3lemt  22655  norm3adifi  22656  normpar  22658  polid  22662  hilablo  22663  hilid  22664  bcs  22684  hlim0  22739  helch  22747  hsn0elch  22751  elch0  22757  hhssnv  22765  ocsh  22786  shscli  22820  choc0  22829  shintcli  22832  pjoc1  22937  pjoc2  22942  h1de2ci  23059  spansn  23062  elspansn  23069  elspansn2  23070  h1datom  23085  spansnj  23150  spansncv  23156  pjch1  23173  pjadji  23188  pjaddi  23189  pjinormi  23190  pjsubi  23191  pjmuli  23192  pjcjt2  23195  pj0i  23196  pjch  23197  pjopyth  23223  pjnorm  23227  pjpyth  23228  pjnel  23229  df0op2  23256  hon0  23297  ho01i  23332  eigre  23339  eigorth  23342  nmopsetn0  23369  nmfnsetn0  23382  dmadjrnb  23410  nmopge0  23415  nmfnge0  23431  bra0  23454  lnop0  23470  lnopmul  23471  0cnop  23483  nmop0  23490  nmfn0  23491  nmop0h  23495  lnopeq0lem2  23510  lnopunii  23516  lnophmi  23522  nmcexi  23530  nmcopexi  23531  lnfn0i  23546  lnfnmuli  23548  nmcfnexi  23555  nlelshi  23564  riesz3i  23566  hmopidmchi  23655  pjss2coi  23668  pjssmi  23669  pjssge0i  23670  pjdifnormi  23671
  Copyright terms: Public domain W3C validator