Axiom ax-hv0cl 22463

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 22384	. 2 class 0h
2		chil 22379	. 2 class ~H
3	1, 2	wcel 1721	1 wff 0h e. ~H

This axiom is referenced by:  hvaddid2  22482  hvmul0  22483  hv2neg  22487  hvsubsub4  22519  hvnegdi  22526  hvsubeq0  22527  hvaddcan  22529  hvsub0  22535  hvsubadd  22536  hi01  22555  hi02  22556  normlem9at  22580  norm0  22587  normsq  22593  normsub0  22595  norm-ii  22597  norm-iii  22599  normsub  22602  normneg  22603  normpyth  22604  norm3difi  22606  norm3dif  22609  norm3lemt  22611  norm3adifi  22612  normpar  22614  polid  22618  hilablo  22619  hilid  22620  bcs  22640  hlim0  22695  helch  22703  hsn0elch  22707  elch0  22713  hhssnv  22721  ocsh  22742  shscli  22776  choc0  22785  shintcli  22788  pjoc1  22893  pjoc2  22898  h1de2ci  23015  spansn  23018  elspansn  23025  elspansn2  23026  h1datom  23041  spansnj  23106  spansncv  23112  pjch1  23129  pjadji  23144  pjaddi  23145  pjinormi  23146  pjsubi  23147  pjmuli  23148  pjcjt2  23151  pj0i  23152  pjch  23153  pjopyth  23179  pjnorm  23183  pjpyth  23184  pjnel  23185  df0op2  23212  hon0  23253  ho01i  23288  eigre  23295  eigorth  23298  nmopsetn0  23325  nmfnsetn0  23338  dmadjrnb  23366  nmopge0  23371  nmfnge0  23387  bra0  23410  lnop0  23426  lnopmul  23427  0cnop  23439  nmop0  23446  nmfn0  23447  nmop0h  23451  lnopeq0lem2  23466  lnopunii  23472  lnophmi  23478  nmcexi  23486  nmcopexi  23487  lnfn0i  23502  lnfnmuli  23504  nmcfnexi  23511  nlelshi  23520  riesz3i  23522  hmopidmchi  23611  pjss2coi  23624  pjssmi  23625  pjssge0i  23626  pjdifnormi  23627