Axiom ax-hv0cl 30973

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 30894	. 2 class 0ℎ
2		chba 30889	. 2 class ℋ
3	1, 2	wcel 2110	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  30992  hvaddlid  30993  hvmul0  30994  hv2neg  30998  hvsub0  31046  hi01  31066  hi02  31067  norm0  31098  normneg  31114  norm3difi  31117  hilablo  31130  hilid  31131  hlim0  31205  helch  31213  hsn0elch  31218  elch0  31224  hhssnv  31234  ocsh  31253  shscli  31287  choc0  31296  shintcli  31299  pj0i  31663  df0op2  31722  hon0  31763  ho01i  31798  nmopsetn0  31835  nmfnsetn0  31848  dmadjrnb  31876  nmopge0  31881  nmfnge0  31897  bra0  31920  lnop0  31936  lnopmul  31937  0cnop  31949  nmop0  31956  nmfn0  31957  nmop0h  31961  nmcexi  31996  nmcopexi  31997  lnfn0i  32012  lnfnmuli  32014  nmcfnexi  32021  nlelshi  32030  riesz3i  32032  hmopidmchi  32121