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

Axiom ax-hv0cl 21508
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 21429 . 2  class  0h
2 chil 21424 . 2  class  ~H
31, 2wcel 1621 1  wff  0h  e.  ~H
Colors of variables: wff set class
This axiom is referenced by:  hvaddid2  21527  hvmul0  21528  hv2neg  21532  hvsubsub4  21564  hvnegdi  21571  hvsubeq0  21572  hvaddcan  21574  hvsub0  21580  hvsubadd  21581  hi01  21600  hi02  21601  normlem9at  21625  norm0  21632  normsq  21638  normsub0  21640  norm-ii  21642  norm-iii  21644  normsub  21647  normneg  21648  normpyth  21649  norm3difi  21651  norm3dif  21654  norm3lemt  21656  norm3adifi  21657  normpar  21659  polid  21663  hilablo  21664  hilid  21665  bcs  21685  hlim0  21740  helch  21748  hsn0elch  21752  elch0  21758  hhssnv  21766  ocsh  21787  shscli  21821  choc0  21830  shintcli  21833  pjoc1  21938  pjoc2  21943  h1de2ci  22060  spansn  22063  elspansn  22070  elspansn2  22071  h1datom  22086  spansnj  22169  spansncv  22175  pjch1  22192  pjadji  22207  pjaddi  22208  pjinormi  22209  pjsubi  22210  pjmuli  22211  pjcjt2  22214  pj0i  22215  pjch  22216  pjopyth  22242  pjnorm  22246  pjpyth  22247  pjnel  22248  df0op2  22257  hon0  22298  ho01i  22333  eigre  22340  eigorth  22343  nmopsetn0  22370  nmfnsetn0  22383  dmadjrnb  22411  nmopge0  22416  nmfnge0  22432  bra0  22455  lnop0  22471  lnopmul  22472  0cnop  22484  nmop0  22491  nmfn0  22492  nmop0h  22496  lnopeq0lem2  22511  lnopunii  22517  lnophmi  22523  nmcexi  22531  nmcopexi  22532  lnfn0i  22547  lnfnmuli  22549  nmcfnexi  22556  nlelshi  22565  riesz3i  22567  hmopidmchi  22656  pjss2coi  22669  pjssmi  22670  pjssge0i  22671  pjdifnormi  22672
  Copyright terms: Public domain W3C validator