Axiom ax-hv0cl 27860

Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hv0cl	⊢ 0ℎ ∈ ℋ

Detailed syntax breakdown of Axiom ax-hv0cl

Step	Hyp	Ref	Expression
1		c0v 27781	. 2 class 0ℎ
2		chil 27776	. 2 class ℋ
3	1, 2	wcel 1990	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  27879  hvaddid2  27880  hvmul0  27881  hv2neg  27885  hvsub0  27933  hi01  27953  hi02  27954  norm0  27985  normneg  28001  norm3difi  28004  hilablo  28017  hilid  28018  hlim0  28092  helch  28100  hsn0elch  28105  elch0  28111  hhssnv  28121  ocsh  28142  shscli  28176  choc0  28185  shintcli  28188  pj0i  28552  df0op2  28611  hon0  28652  ho01i  28687  nmopsetn0  28724  nmfnsetn0  28737  dmadjrnb  28765  nmopge0  28770  nmfnge0  28786  bra0  28809  lnop0  28825  lnopmul  28826  0cnop  28838  nmop0  28845  nmfn0  28846  nmop0h  28850  nmcexi  28885  nmcopexi  28886  lnfn0i  28901  lnfnmuli  28903  nmcfnexi  28910  nlelshi  28919  riesz3i  28921  hmopidmchi  29010