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

Axiom ax-hv0cl 22463
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 22384 . 2  class  0h
2 chil 22379 . 2  class  ~H
31, 2wcel 1721 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22482  hvmul0  22483  hv2neg  22487  hvsubsub4  22519  hvnegdi  22526  hvsubeq0  22527  hvaddcan  22529  hvsub0  22535  hvsubadd  22536  hi01  22555  hi02  22556  normlem9at  22580  norm0  22587  normsq  22593  normsub0  22595  norm-ii  22597  norm-iii  22599  normsub  22602  normneg  22603  normpyth  22604  norm3difi  22606  norm3dif  22609  norm3lemt  22611  norm3adifi  22612  normpar  22614  polid  22618  hilablo  22619  hilid  22620  bcs  22640  hlim0  22695  helch  22703  hsn0elch  22707  elch0  22713  hhssnv  22721  ocsh  22742  shscli  22776  choc0  22785  shintcli  22788  pjoc1  22893  pjoc2  22898  h1de2ci  23015  spansn  23018  elspansn  23025  elspansn2  23026  h1datom  23041  spansnj  23106  spansncv  23112  pjch1  23129  pjadji  23144  pjaddi  23145  pjinormi  23146  pjsubi  23147  pjmuli  23148  pjcjt2  23151  pj0i  23152  pjch  23153  pjopyth  23179  pjnorm  23183  pjpyth  23184  pjnel  23185  df0op2  23212  hon0  23253  ho01i  23288  eigre  23295  eigorth  23298  nmopsetn0  23325  nmfnsetn0  23338  dmadjrnb  23366  nmopge0  23371  nmfnge0  23387  bra0  23410  lnop0  23426  lnopmul  23427  0cnop  23439  nmop0  23446  nmfn0  23447  nmop0h  23451  lnopeq0lem2  23466  lnopunii  23472  lnophmi  23478  nmcexi  23486  nmcopexi  23487  lnfn0i  23502  lnfnmuli  23504  nmcfnexi  23511  nlelshi  23520  riesz3i  23522  hmopidmchi  23611  pjss2coi  23624  pjssmi  23625  pjssge0i  23626  pjdifnormi  23627
  Copyright terms: Public domain W3C validator