Axiom ax-hv0cl 30930

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

This axiom is referenced by:  ifhvhv0  30949  hvaddlid  30950  hvmul0  30951  hv2neg  30955  hvsub0  31003  hi01  31023  hi02  31024  norm0  31055  normneg  31071  norm3difi  31074  hilablo  31087  hilid  31088  hlim0  31162  helch  31170  hsn0elch  31175  elch0  31181  hhssnv  31191  ocsh  31210  shscli  31244  choc0  31253  shintcli  31256  pj0i  31620  df0op2  31679  hon0  31720  ho01i  31755  nmopsetn0  31792  nmfnsetn0  31805  dmadjrnb  31833  nmopge0  31838  nmfnge0  31854  bra0  31877  lnop0  31893  lnopmul  31894  0cnop  31906  nmop0  31913  nmfn0  31914  nmop0h  31918  nmcexi  31953  nmcopexi  31954  lnfn0i  31969  lnfnmuli  31971  nmcfnexi  31978  nlelshi  31987  riesz3i  31989  hmopidmchi  32078