Axiom ax-hv0cl 31022

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 30943	. 2 class 0ℎ
2		chba 30938	. 2 class ℋ
3	1, 2	wcel 2108	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31041  hvaddlid  31042  hvmul0  31043  hv2neg  31047  hvsub0  31095  hi01  31115  hi02  31116  norm0  31147  normneg  31163  norm3difi  31166  hilablo  31179  hilid  31180  hlim0  31254  helch  31262  hsn0elch  31267  elch0  31273  hhssnv  31283  ocsh  31302  shscli  31336  choc0  31345  shintcli  31348  pj0i  31712  df0op2  31771  hon0  31812  ho01i  31847  nmopsetn0  31884  nmfnsetn0  31897  dmadjrnb  31925  nmopge0  31930  nmfnge0  31946  bra0  31969  lnop0  31985  lnopmul  31986  0cnop  31998  nmop0  32005  nmfn0  32006  nmop0h  32010  nmcexi  32045  nmcopexi  32046  lnfn0i  32061  lnfnmuli  32063  nmcfnexi  32070  nlelshi  32079  riesz3i  32081  hmopidmchi  32170