Axiom ax-hv0cl 31635

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 31556	. 2 class 0ℎ
2		chba 31551	. 2 class ℋ
3	1, 2	wcel 2147	1 wff 0ℎ ∈ ℋ

This axiom is used by:  ifhvhv0  31654  hvaddlid  31655  hvmul0  31656  hv2neg  31660  hvsub0  31708  hi01  31728  hi02  31729  norm0  31760  normneg  31776  norm3difi  31779  hilablo  31792  hilid  31793  hlim0  31867  helch  31875  hsn0elch  31880  elch0  31886  hhssnv  31896  ocsh  31915  shscli  31949  choc0  31958  shintcli  31961  pj0i  32325  df0op2  32384  hon0  32425  ho01i  32460  nmopsetn0  32497  nmfnsetn0  32510  dmadjrnb  32538  nmopge0  32543  nmfnge0  32559  bra0  32582  lnop0  32598  lnopmul  32599  0cnop  32611  nmop0  32618  nmfn0  32619  nmop0h  32623  nmcexi  32658  nmcopexi  32659  lnfn0i  32674  lnfnmuli  32676  nmcfnexi  32683  nlelshi  32692  riesz3i  32694  hmopidmchi  32783