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

Axiom ax-hv0cl 22355
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 22276 . 2  class  0h
2 chil 22271 . 2  class  ~H
31, 2wcel 1717 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22374  hvmul0  22375  hv2neg  22379  hvsubsub4  22411  hvnegdi  22418  hvsubeq0  22419  hvaddcan  22421  hvsub0  22427  hvsubadd  22428  hi01  22447  hi02  22448  normlem9at  22472  norm0  22479  normsq  22485  normsub0  22487  norm-ii  22489  norm-iii  22491  normsub  22494  normneg  22495  normpyth  22496  norm3difi  22498  norm3dif  22501  norm3lemt  22503  norm3adifi  22504  normpar  22506  polid  22510  hilablo  22511  hilid  22512  bcs  22532  hlim0  22587  helch  22595  hsn0elch  22599  elch0  22605  hhssnv  22613  ocsh  22634  shscli  22668  choc0  22677  shintcli  22680  pjoc1  22785  pjoc2  22790  h1de2ci  22907  spansn  22910  elspansn  22917  elspansn2  22918  h1datom  22933  spansnj  22998  spansncv  23004  pjch1  23021  pjadji  23036  pjaddi  23037  pjinormi  23038  pjsubi  23039  pjmuli  23040  pjcjt2  23043  pj0i  23044  pjch  23045  pjopyth  23071  pjnorm  23075  pjpyth  23076  pjnel  23077  df0op2  23104  hon0  23145  ho01i  23180  eigre  23187  eigorth  23190  nmopsetn0  23217  nmfnsetn0  23230  dmadjrnb  23258  nmopge0  23263  nmfnge0  23279  bra0  23302  lnop0  23318  lnopmul  23319  0cnop  23331  nmop0  23338  nmfn0  23339  nmop0h  23343  lnopeq0lem2  23358  lnopunii  23364  lnophmi  23370  nmcexi  23378  nmcopexi  23379  lnfn0i  23394  lnfnmuli  23396  nmcfnexi  23403  nlelshi  23412  riesz3i  23414  hmopidmchi  23503  pjss2coi  23516  pjssmi  23517  pjssge0i  23518  pjdifnormi  23519
  Copyright terms: Public domain W3C validator