Axiom ax-hv0cl 8873

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 8791	. 2 class 0h
2		chil 8788	. 2 class H~
3	1, 2	wcel 958	1 wff 0h e. H~

This axiom is referenced by:  hvaddid2t 8892  hvmul0t 8893  hv2negt 8897  hvsubsub4t 8927  hvnegdit 8934  hvsubeq0t 8935  hvaddcant 8937  hvsub0t 8943  hvsubaddt 8944  hi01t 8962  hi02t 8963  normlem9at 8987  norm0 8995  normsqt 9001  normsub0t 9003  norm-iit 9005  norm-iiit 9007  normsubt 9010  normnegt 9011  normpytht 9012  norm3dif 9014  norm3dift 9017  norm3lemt 9019  norm3adift 9020  normpart 9022  polidt 9026  hilabl 9027  hilid 9028  bcst 9048  hlim0 9105  hlimcau 9107  hlimuni 9109  helch 9116  hsn0elch 9120  elch0 9126  hhssnv 9134  ocsh 9156  occllem2 9174  occllem8 9180  projlem8 9193  pjthlem13 9231  pjtht 9234  axpjpjt 9256  pjoc1t 9267  pjoc2t 9272  shscl 9281  choc0 9290  shintcl 9293  h1de2ct 9479  spansnt 9482  elspansnt 9489  elspansn2t 9490  h1datomt 9505  spansnjt 9592  spansncvt 9598  pjch1t 9615  pjadjt 9630  pjaddt 9631  pjinormt 9632  pjsubt 9633  pjmult 9634  pjcjt2 9637  pj0 9638  pjcht 9639  pjopytht 9665  pjnormt 9669  pjpytht 9670  pjnelt 9671  df0op2 9678  hon0 9719  ho01 9754  eigret 9761  eigortht 9764  nmopsetn0 9792  nmfnsetn0 9805  dmadjrnb 9830  nmopge0t 9835  nmfnge0t 9851  bra0 9874  lnop0t 9890  lnopmult 9891  0cnop 9903  nmop0 9910  nmfn0 9911  nmop0h 9916  lnopeq0lem2 9931  lnopuni 9937  lnophm 9943  nmcopexlem2 9952  lnfn0 9971  lnfnmul 9973  nmcfnexlem2 9981  nlelsh 9993  riesz3 9995  hmopidmch 10079  pjss2co 10092  pjssmt 10093  pjssge0t 10094  pjdifnormt 10095

Copyright terms: Public domain