Axiom ax-hvzercl 4987

Description: The zero vector is in the vector space.

Assertion

Ref	Expression
ax-hvzercl	⊢ 0v ∈ ℋ

Detailed syntax breakdown of Axiom ax-hvzercl

Step	Hyp	Ref	Expression
1		c0v 4961	. 2 class 0v
2		chil 4958	. 2 class ℋ
3	1, 2	wcel 1092	1 wff 0v ∈ ℋ

This axiom is referenced by:  hvaddid2t 5003  hvmul0t 5004  hv2neg 5010  hvsubsub4t 5032  hvnegdit 5039  hvsubeq0t 5040  hvsub0t 5041  hvsubaddt 5042  hizer1t 5054  hizer2t 5055  norm0 5079  normsub0t 5085  norm-iiit 5088  normsubt 5091  normpytht 5092  norm3dif 5094  norm3lemt 5097  norm3adift 5098  hlim0 5140  hlimcau 5142  hlimuni 5144  helch 5151  hsn0elch 5155  elch0 5158  ocsh 5164  occllem2 5181  occllem8 5187  projlem8 5200  pjthlem13 5237  pjtht 5240  axpjpjt 5260  pjoc1t 5270  pjoc2t 5274  shscl 5282  choc0 5291  shintcl 5294  h1de2ct 5461  spansnt 5464  elspansnt 5471  elspansn2t 5472  h1datomt 5484  spansnjt 5540  spansncvt 5543  pjch1t 5560  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pj0 5581  pjcht 5582  ho0 5612  pjss2co 5634  pjssmt 5635  pjssge0t 5636  pjdifnormt 5637  pjopytht 5662  pjnormt 5666  pjnelt 5667

metamath.org