Axiom ax-hv0cl 31538

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 31459	. 2 class 0ℎ
2		chba 31454	. 2 class ℋ
3	1, 2	wcel 2145	1 wff 0ℎ ∈ ℋ

This axiom is used by:  ifhvhv0  31557  hvaddlid  31558  hvmul0  31559  hv2neg  31563  hvsub0  31611  hi01  31631  hi02  31632  norm0  31663  normneg  31679  norm3difi  31682  hilablo  31695  hilid  31696  hlim0  31770  helch  31778  hsn0elch  31783  elch0  31789  hhssnv  31799  ocsh  31818  shscli  31852  choc0  31861  shintcli  31864  pj0i  32228  df0op2  32287  hon0  32328  ho01i  32363  nmopsetn0  32400  nmfnsetn0  32413  dmadjrnb  32441  nmopge0  32446  nmfnge0  32462  bra0  32485  lnop0  32501  lnopmul  32502  0cnop  32514  nmop0  32521  nmfn0  32522  nmop0h  32526  nmcexi  32561  nmcopexi  32562  lnfn0i  32577  lnfnmuli  32579  nmcfnexi  32586  nlelshi  32595  riesz3i  32597  hmopidmchi  32686