Axiom ax-hv0cl 21583

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 21504	. 2 class 0h
2		chil 21499	. 2 class ~H
3	1, 2	wcel 1684	1 wff 0h e. ~H

This axiom is referenced by:  hvaddid2  21602  hvmul0  21603  hv2neg  21607  hvsubsub4  21639  hvnegdi  21646  hvsubeq0  21647  hvaddcan  21649  hvsub0  21655  hvsubadd  21656  hi01  21675  hi02  21676  normlem9at  21700  norm0  21707  normsq  21713  normsub0  21715  norm-ii  21717  norm-iii  21719  normsub  21722  normneg  21723  normpyth  21724  norm3difi  21726  norm3dif  21729  norm3lemt  21731  norm3adifi  21732  normpar  21734  polid  21738  hilablo  21739  hilid  21740  bcs  21760  hlim0  21815  helch  21823  hsn0elch  21827  elch0  21833  hhssnv  21841  ocsh  21862  shscli  21896  choc0  21905  shintcli  21908  pjoc1  22013  pjoc2  22018  h1de2ci  22135  spansn  22138  elspansn  22145  elspansn2  22146  h1datom  22161  spansnj  22226  spansncv  22232  pjch1  22249  pjadji  22264  pjaddi  22265  pjinormi  22266  pjsubi  22267  pjmuli  22268  pjcjt2  22271  pj0i  22272  pjch  22273  pjopyth  22299  pjnorm  22303  pjpyth  22304  pjnel  22305  df0op2  22332  hon0  22373  ho01i  22408  eigre  22415  eigorth  22418  nmopsetn0  22445  nmfnsetn0  22458  dmadjrnb  22486  nmopge0  22491  nmfnge0  22507  bra0  22530  lnop0  22546  lnopmul  22547  0cnop  22559  nmop0  22566  nmfn0  22567  nmop0h  22571  lnopeq0lem2  22586  lnopunii  22592  lnophmi  22598  nmcexi  22606  nmcopexi  22607  lnfn0i  22622  lnfnmuli  22624  nmcfnexi  22631  nlelshi  22640  riesz3i  22642  hmopidmchi  22731  pjss2coi  22744  pjssmi  22745  pjssge0i  22746  pjdifnormi  22747