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

Axiom ax-hv0cl 22459
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 22380 . 2  class  0h
2 chil 22375 . 2  class  ~H
31, 2wcel 1721 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  22478  hvmul0  22479  hv2neg  22483  hvsubsub4  22515  hvnegdi  22522  hvsubeq0  22523  hvaddcan  22525  hvsub0  22531  hvsubadd  22532  hi01  22551  hi02  22552  normlem9at  22576  norm0  22583  normsq  22589  normsub0  22591  norm-ii  22593  norm-iii  22595  normsub  22598  normneg  22599  normpyth  22600  norm3difi  22602  norm3dif  22605  norm3lemt  22607  norm3adifi  22608  normpar  22610  polid  22614  hilablo  22615  hilid  22616  bcs  22636  hlim0  22691  helch  22699  hsn0elch  22703  elch0  22709  hhssnv  22717  ocsh  22738  shscli  22772  choc0  22781  shintcli  22784  pjoc1  22889  pjoc2  22894  h1de2ci  23011  spansn  23014  elspansn  23021  elspansn2  23022  h1datom  23037  spansnj  23102  spansncv  23108  pjch1  23125  pjadji  23140  pjaddi  23141  pjinormi  23142  pjsubi  23143  pjmuli  23144  pjcjt2  23147  pj0i  23148  pjch  23149  pjopyth  23175  pjnorm  23179  pjpyth  23180  pjnel  23181  df0op2  23208  hon0  23249  ho01i  23284  eigre  23291  eigorth  23294  nmopsetn0  23321  nmfnsetn0  23334  dmadjrnb  23362  nmopge0  23367  nmfnge0  23383  bra0  23406  lnop0  23422  lnopmul  23423  0cnop  23435  nmop0  23442  nmfn0  23443  nmop0h  23447  lnopeq0lem2  23462  lnopunii  23468  lnophmi  23474  nmcexi  23482  nmcopexi  23483  lnfn0i  23498  lnfnmuli  23500  nmcfnexi  23507  nlelshi  23516  riesz3i  23518  hmopidmchi  23607  pjss2coi  23620  pjssmi  23621  pjssge0i  23622  pjdifnormi  23623
  Copyright terms: Public domain W3C validator