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

Axiom ax-hv0cl 22506
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 22427 . 2  class  0h
2 chil 22422 . 2  class  ~H
31, 2wcel 1725 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22525  hvmul0  22526  hv2neg  22530  hvsubsub4  22562  hvnegdi  22569  hvsubeq0  22570  hvaddcan  22572  hvsub0  22578  hvsubadd  22579  hi01  22598  hi02  22599  normlem9at  22623  norm0  22630  normsq  22636  normsub0  22638  norm-ii  22640  norm-iii  22642  normsub  22645  normneg  22646  normpyth  22647  norm3difi  22649  norm3dif  22652  norm3lemt  22654  norm3adifi  22655  normpar  22657  polid  22661  hilablo  22662  hilid  22663  bcs  22683  hlim0  22738  helch  22746  hsn0elch  22750  elch0  22756  hhssnv  22764  ocsh  22785  shscli  22819  choc0  22828  shintcli  22831  pjoc1  22936  pjoc2  22941  h1de2ci  23058  spansn  23061  elspansn  23068  elspansn2  23069  h1datom  23084  spansnj  23149  spansncv  23155  pjch1  23172  pjadji  23187  pjaddi  23188  pjinormi  23189  pjsubi  23190  pjmuli  23191  pjcjt2  23194  pj0i  23195  pjch  23196  pjopyth  23222  pjnorm  23226  pjpyth  23227  pjnel  23228  df0op2  23255  hon0  23296  ho01i  23331  eigre  23338  eigorth  23341  nmopsetn0  23368  nmfnsetn0  23381  dmadjrnb  23409  nmopge0  23414  nmfnge0  23430  bra0  23453  lnop0  23469  lnopmul  23470  0cnop  23482  nmop0  23489  nmfn0  23490  nmop0h  23494  lnopeq0lem2  23509  lnopunii  23515  lnophmi  23521  nmcexi  23529  nmcopexi  23530  lnfn0i  23545  lnfnmuli  23547  nmcfnexi  23554  nlelshi  23563  riesz3i  23565  hmopidmchi  23654  pjss2coi  23667  pjssmi  23668  pjssge0i  23669  pjdifnormi  23670
  Copyright terms: Public domain W3C validator