Axiom ax-hv0cl 30932

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 30853	. 2 class 0ℎ
2		chba 30848	. 2 class ℋ
3	1, 2	wcel 2109	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  30951  hvaddlid  30952  hvmul0  30953  hv2neg  30957  hvsub0  31005  hi01  31025  hi02  31026  norm0  31057  normneg  31073  norm3difi  31076  hilablo  31089  hilid  31090  hlim0  31164  helch  31172  hsn0elch  31177  elch0  31183  hhssnv  31193  ocsh  31212  shscli  31246  choc0  31255  shintcli  31258  pj0i  31622  df0op2  31681  hon0  31722  ho01i  31757  nmopsetn0  31794  nmfnsetn0  31807  dmadjrnb  31835  nmopge0  31840  nmfnge0  31856  bra0  31879  lnop0  31895  lnopmul  31896  0cnop  31908  nmop0  31915  nmfn0  31916  nmop0h  31920  nmcexi  31955  nmcopexi  31956  lnfn0i  31971  lnfnmuli  31973  nmcfnexi  31980  nlelshi  31989  riesz3i  31991  hmopidmchi  32080