Axiom ax-hv0cl 28780

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 28701	. 2 class 0ℎ
2		chba 28696	. 2 class ℋ
3	1, 2	wcel 2114	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  28799  hvaddid2  28800  hvmul0  28801  hv2neg  28805  hvsub0  28853  hi01  28873  hi02  28874  norm0  28905  normneg  28921  norm3difi  28924  hilablo  28937  hilid  28938  hlim0  29012  helch  29020  hsn0elch  29025  elch0  29031  hhssnv  29041  ocsh  29060  shscli  29094  choc0  29103  shintcli  29106  pj0i  29470  df0op2  29529  hon0  29570  ho01i  29605  nmopsetn0  29642  nmfnsetn0  29655  dmadjrnb  29683  nmopge0  29688  nmfnge0  29704  bra0  29727  lnop0  29743  lnopmul  29744  0cnop  29756  nmop0  29763  nmfn0  29764  nmop0h  29768  nmcexi  29803  nmcopexi  29804  lnfn0i  29819  lnfnmuli  29821  nmcfnexi  29828  nlelshi  29837  riesz3i  29839  hmopidmchi  29928