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

Axiom ax-hv0cl 21599
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 21520 . 2  class  0h
2 chil 21515 . 2  class  ~H
31, 2wcel 1696 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  21618  hvmul0  21619  hv2neg  21623  hvsubsub4  21655  hvnegdi  21662  hvsubeq0  21663  hvaddcan  21665  hvsub0  21671  hvsubadd  21672  hi01  21691  hi02  21692  normlem9at  21716  norm0  21723  normsq  21729  normsub0  21731  norm-ii  21733  norm-iii  21735  normsub  21738  normneg  21739  normpyth  21740  norm3difi  21742  norm3dif  21745  norm3lemt  21747  norm3adifi  21748  normpar  21750  polid  21754  hilablo  21755  hilid  21756  bcs  21776  hlim0  21831  helch  21839  hsn0elch  21843  elch0  21849  hhssnv  21857  ocsh  21878  shscli  21912  choc0  21921  shintcli  21924  pjoc1  22029  pjoc2  22034  h1de2ci  22151  spansn  22154  elspansn  22161  elspansn2  22162  h1datom  22177  spansnj  22242  spansncv  22248  pjch1  22265  pjadji  22280  pjaddi  22281  pjinormi  22282  pjsubi  22283  pjmuli  22284  pjcjt2  22287  pj0i  22288  pjch  22289  pjopyth  22315  pjnorm  22319  pjpyth  22320  pjnel  22321  df0op2  22348  hon0  22389  ho01i  22424  eigre  22431  eigorth  22434  nmopsetn0  22461  nmfnsetn0  22474  dmadjrnb  22502  nmopge0  22507  nmfnge0  22523  bra0  22546  lnop0  22562  lnopmul  22563  0cnop  22575  nmop0  22582  nmfn0  22583  nmop0h  22587  lnopeq0lem2  22602  lnopunii  22608  lnophmi  22614  nmcexi  22622  nmcopexi  22623  lnfn0i  22638  lnfnmuli  22640  nmcfnexi  22647  nlelshi  22656  riesz3i  22658  hmopidmchi  22747  pjss2coi  22760  pjssmi  22761  pjssge0i  22762  pjdifnormi  22763
  Copyright terms: Public domain W3C validator