Axiom ax-hv0cl 30990

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 30911	. 2 class 0ℎ
2		chba 30906	. 2 class ℋ
3	1, 2	wcel 2111	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31009  hvaddlid  31010  hvmul0  31011  hv2neg  31015  hvsub0  31063  hi01  31083  hi02  31084  norm0  31115  normneg  31131  norm3difi  31134  hilablo  31147  hilid  31148  hlim0  31222  helch  31230  hsn0elch  31235  elch0  31241  hhssnv  31251  ocsh  31270  shscli  31304  choc0  31313  shintcli  31316  pj0i  31680  df0op2  31739  hon0  31780  ho01i  31815  nmopsetn0  31852  nmfnsetn0  31865  dmadjrnb  31893  nmopge0  31898  nmfnge0  31914  bra0  31937  lnop0  31953  lnopmul  31954  0cnop  31966  nmop0  31973  nmfn0  31974  nmop0h  31978  nmcexi  32013  nmcopexi  32014  lnfn0i  32029  lnfnmuli  32031  nmcfnexi  32038  nlelshi  32047  riesz3i  32049  hmopidmchi  32138