Axiom ax-hv0cl 31213

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 31134	. 2 class 0ℎ
2		chba 31129	. 2 class ℋ
3	1, 2	wcel 2143	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31232  hvaddlid  31233  hvmul0  31234  hv2neg  31238  hvsub0  31286  hi01  31306  hi02  31307  norm0  31338  normneg  31354  norm3difi  31357  hilablo  31370  hilid  31371  hlim0  31445  helch  31453  hsn0elch  31458  elch0  31464  hhssnv  31474  ocsh  31493  shscli  31527  choc0  31536  shintcli  31539  pj0i  31903  df0op2  31962  hon0  32003  ho01i  32038  nmopsetn0  32075  nmfnsetn0  32088  dmadjrnb  32116  nmopge0  32121  nmfnge0  32137  bra0  32160  lnop0  32176  lnopmul  32177  0cnop  32189  nmop0  32196  nmfn0  32197  nmop0h  32201  nmcexi  32236  nmcopexi  32237  lnfn0i  32252  lnfnmuli  32254  nmcfnexi  32261  nlelshi  32270  riesz3i  32272  hmopidmchi  32361