Axiom ax-hv0cl 8812

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 8730	. 2 class 0h
2		chil 8727	. 2 class H~
3	1, 2	wcel 956	1 wff 0h e. H~

This axiom is referenced by:  hvaddid2t 8831  hvmul0t 8832  hv2negt 8836  hvsubsub4t 8866  hvnegdit 8873  hvsubeq0t 8874  hvaddcant 8876  hvsub0t 8882  hvsubaddt 8883  hi01t 8901  hi02t 8902  normlem9at 8926  norm0 8934  normsqt 8940  normsub0t 8942  norm-iit 8944  norm-iiit 8946  normsubt 8949  normnegt 8950  normpytht 8951  norm3dif 8953  norm3dift 8956  norm3lemt 8958  norm3adift 8959  normpart 8961  polidt 8965  hilabl 8966  hilid 8967  bcst 8987  hlim0 9044  hlimcau 9046  hlimuni 9048  helch 9055  hsn0elch 9059  elch0 9065  hhssnv 9073  ocsh 9095  occllem2 9113  occllem8 9119  projlem8 9132  pjthlem13 9169  pjtht 9172  axpjpjt 9194  pjoc1t 9205  pjoc2t 9210  shscl 9219  choc0 9228  shintcl 9231  h1de2ct 9418  spansnt 9421  elspansnt 9428  elspansn2t 9429  h1datomt 9445  spansnjt 9532  spansncvt 9538  pjch1t 9555  pjadjt 9570  pjaddt 9571  pjinormt 9572  pjsubt 9573  pjmult 9574  pjcjt2 9577  pj0 9578  pjcht 9579  pjopytht 9605  pjnormt 9609  pjpytht 9610  pjnelt 9611  df0op2 9618  hon0 9659  ho01 9694  eigret 9701  eigortht 9704  nmopsetn0 9732  nmfnsetn0 9745  dmadjrnb 9770  nmopge0t 9774  nmfnge0t 9790  bra0 9813  lnop0t 9829  lnopmult 9830  0cnop 9842  nmop0 9849  nmfn0 9850  nmop0h 9854  lnopeq0lem2 9869  lnopuni 9875  lnophm 9881  nmcopexlem2 9890  lnfn0 9909  lnfnmul 9911  nmcfnexlem2 9919  nlelsh 9931  riesz3 9933  hmopidmch 10017  pjss2co 10030  pjssmt 10031  pjssge0t 10032  pjdifnormt 10033

Copyright terms: Public domain