Axiom ax-hv0cl 21577

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

Step	Hyp	Ref	Expression
1		c0v 21498	. 2 class 0h
2		chil 21493	. 2 class ~H
3	1, 2	wcel 1687	1 wff 0h e. ~H

This axiom is referenced by:  hvaddid2  21596  hvmul0  21597  hv2neg  21601  hvsubsub4  21633  hvnegdi  21640  hvsubeq0  21641  hvaddcan  21643  hvsub0  21649  hvsubadd  21650  hi01  21669  hi02  21670  normlem9at  21694  norm0  21701  normsq  21707  normsub0  21709  norm-ii  21711  norm-iii  21713  normsub  21716  normneg  21717  normpyth  21718  norm3difi  21720  norm3dif  21723  norm3lemt  21725  norm3adifi  21726  normpar  21728  polid  21732  hilablo  21733  hilid  21734  bcs  21754  hlim0  21809  helch  21817  hsn0elch  21821  elch0  21827  hhssnv  21835  ocsh  21856  shscli  21890  choc0  21899  shintcli  21902  pjoc1  22007  pjoc2  22012  h1de2ci  22129  spansn  22132  elspansn  22139  elspansn2  22140  h1datom  22155  spansnj  22220  spansncv  22226  pjch1  22243  pjadji  22258  pjaddi  22259  pjinormi  22260  pjsubi  22261  pjmuli  22262  pjcjt2  22265  pj0i  22266  pjch  22267  pjopyth  22293  pjnorm  22297  pjpyth  22298  pjnel  22299  df0op2  22326  hon0  22367  ho01i  22402  eigre  22409  eigorth  22412  nmopsetn0  22439  nmfnsetn0  22452  dmadjrnb  22480  nmopge0  22485  nmfnge0  22501  bra0  22524  lnop0  22540  lnopmul  22541  0cnop  22553  nmop0  22560  nmfn0  22561  nmop0h  22565  lnopeq0lem2  22580  lnopunii  22586  lnophmi  22592  nmcexi  22600  nmcopexi  22601  lnfn0i  22616  lnfnmuli  22618  nmcfnexi  22625  nlelshi  22634  riesz3i  22636  hmopidmchi  22725  pjss2coi  22738  pjssmi  22739  pjssge0i  22740  pjdifnormi  22741