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

Axiom ax-hv0cl 21413
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 21334 . 2  class  0h
2 chil 21329 . 2  class  ~H
31, 2wcel 1621 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  21432  hvmul0  21433  hv2neg  21437  hvsubsub4  21469  hvnegdi  21476  hvsubeq0  21477  hvaddcan  21479  hvsub0  21485  hvsubadd  21486  hi01  21505  hi02  21506  normlem9at  21530  norm0  21537  normsq  21543  normsub0  21545  norm-ii  21547  norm-iii  21549  normsub  21552  normneg  21553  normpyth  21554  norm3difi  21556  norm3dif  21559  norm3lemt  21561  norm3adifi  21562  normpar  21564  polid  21568  hilablo  21569  hilid  21570  bcs  21590  hlim0  21645  helch  21653  hsn0elch  21657  elch0  21663  hhssnv  21671  ocsh  21692  shscli  21726  choc0  21735  shintcli  21738  pjoc1  21843  pjoc2  21848  h1de2ci  21965  spansn  21968  elspansn  21975  elspansn2  21976  h1datom  21991  spansnj  22074  spansncv  22080  pjch1  22097  pjadji  22112  pjaddi  22113  pjinormi  22114  pjsubi  22115  pjmuli  22116  pjcjt2  22119  pj0i  22120  pjch  22121  pjopyth  22147  pjnorm  22151  pjpyth  22152  pjnel  22153  df0op2  22162  hon0  22203  ho01i  22238  eigre  22245  eigorth  22248  nmopsetn0  22275  nmfnsetn0  22288  dmadjrnb  22316  nmopge0  22321  nmfnge0  22337  bra0  22360  lnop0  22376  lnopmul  22377  0cnop  22389  nmop0  22396  nmfn0  22397  nmop0h  22401  lnopeq0lem2  22416  lnopunii  22422  lnophmi  22428  nmcexi  22436  nmcopexi  22437  lnfn0i  22452  lnfnmuli  22454  nmcfnexi  22461  nlelshi  22470  riesz3i  22472  hmopidmchi  22561  pjss2coi  22574  pjssmi  22575  pjssge0i  22576  pjdifnormi  22577
  Copyright terms: Public domain W3C validator