Axiom ax-hv0cl 21529

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 21450	. 2 class 0h
2		chil 21445	. 2 class ~H
3	1, 2	wcel 1621	1 wff 0h e. ~H

This axiom is referenced by:  hvaddid2  21548  hvmul0  21549  hv2neg  21553  hvsubsub4  21585  hvnegdi  21592  hvsubeq0  21593  hvaddcan  21595  hvsub0  21601  hvsubadd  21602  hi01  21621  hi02  21622  normlem9at  21646  norm0  21653  normsq  21659  normsub0  21661  norm-ii  21663  norm-iii  21665  normsub  21668  normneg  21669  normpyth  21670  norm3difi  21672  norm3dif  21675  norm3lemt  21677  norm3adifi  21678  normpar  21680  polid  21684  hilablo  21685  hilid  21686  bcs  21706  hlim0  21761  helch  21769  hsn0elch  21773  elch0  21779  hhssnv  21787  ocsh  21808  shscli  21842  choc0  21851  shintcli  21854  pjoc1  21959  pjoc2  21964  h1de2ci  22081  spansn  22084  elspansn  22091  elspansn2  22092  h1datom  22107  spansnj  22190  spansncv  22196  pjch1  22213  pjadji  22228  pjaddi  22229  pjinormi  22230  pjsubi  22231  pjmuli  22232  pjcjt2  22235  pj0i  22236  pjch  22237  pjopyth  22263  pjnorm  22267  pjpyth  22268  pjnel  22269  df0op2  22278  hon0  22319  ho01i  22354  eigre  22361  eigorth  22364  nmopsetn0  22391  nmfnsetn0  22404  dmadjrnb  22432  nmopge0  22437  nmfnge0  22453  bra0  22476  lnop0  22492  lnopmul  22493  0cnop  22505  nmop0  22512  nmfn0  22513  nmop0h  22517  lnopeq0lem2  22532  lnopunii  22538  lnophmi  22544  nmcexi  22552  nmcopexi  22553  lnfn0i  22568  lnfnmuli  22570  nmcfnexi  22577  nlelshi  22586  riesz3i  22588  hmopidmchi  22677  pjss2coi  22690  pjssmi  22691  pjssge0i  22692  pjdifnormi  22693