Axiom ax-hv0cl 8828

Description: The zero vector is in the vector space.

Assertion

Ref	Expression
ax-hv0cl	|- 0h e. H~

Detailed syntax breakdown of Axiom ax-hv0cl

Step	Hyp	Ref	Expression
1		c0v 8746	. 2 class 0h
2		chil 8743	. 2 class H~
3	1, 2	wcel 958	1 wff 0h e. H~

This axiom is referenced by:  hvaddid2t 8847  hvmul0t 8848  hv2negt 8852  hvsubsub4t 8882  hvnegdit 8889  hvsubeq0t 8890  hvaddcant 8892  hvsub0t 8898  hvsubaddt 8899  hi01t 8917  hi02t 8918  normlem9at 8942  norm0 8950  normsqt 8956  normsub0t 8958  norm-iit 8960  norm-iiit 8962  normsubt 8965  normnegt 8966  normpytht 8967  norm3dif 8969  norm3dift 8972  norm3lemt 8974  norm3adift 8975  normpart 8977  polidt 8981  hilabl 8982  hilid 8983  bcst 9003  hlim0 9060  hlimcau 9062  hlimuni 9064  helch 9071  hsn0elch 9075  elch0 9081  hhssnv 9089  ocsh 9111  occllem2 9129  occllem8 9135  projlem8 9148  pjthlem13 9186  pjtht 9189  axpjpjt 9211  pjoc1t 9222  pjoc2t 9227  shscl 9236  choc0 9245  shintcl 9248  h1de2ct 9434  spansnt 9437  elspansnt 9444  elspansn2t 9445  h1datomt 9460  spansnjt 9547  spansncvt 9553  pjch1t 9570  pjadjt 9585  pjaddt 9586  pjinormt 9587  pjsubt 9588  pjmult 9589  pjcjt2 9592  pj0 9593  pjcht 9594  pjopytht 9620  pjnormt 9624  pjpytht 9625  pjnelt 9626  df0op2 9633  hon0 9674  ho01 9709  eigret 9716  eigortht 9719  nmopsetn0 9747  nmfnsetn0 9760  dmadjrnb 9785  nmopge0t 9790  nmfnge0t 9806  bra0 9829  lnop0t 9845  lnopmult 9846  0cnop 9858  nmop0 9865  nmfn0 9866  nmop0h 9871  lnopeq0lem2 9886  lnopuni 9892  lnophm 9898  nmcopexlem2 9907  lnfn0 9926  lnfnmul 9928  nmcfnexlem2 9936  nlelsh 9948  riesz3 9950  hmopidmch 10034  pjss2co 10047  pjssmt 10048  pjssge0t 10049  pjdifnormt 10050

Copyright terms: Public domain