Axiom ax-hv0cl 28786

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

This axiom is referenced by:  ifhvhv0  28805  hvaddid2  28806  hvmul0  28807  hv2neg  28811  hvsub0  28859  hi01  28879  hi02  28880  norm0  28911  normneg  28927  norm3difi  28930  hilablo  28943  hilid  28944  hlim0  29018  helch  29026  hsn0elch  29031  elch0  29037  hhssnv  29047  ocsh  29066  shscli  29100  choc0  29109  shintcli  29112  pj0i  29476  df0op2  29535  hon0  29576  ho01i  29611  nmopsetn0  29648  nmfnsetn0  29661  dmadjrnb  29689  nmopge0  29694  nmfnge0  29710  bra0  29733  lnop0  29749  lnopmul  29750  0cnop  29762  nmop0  29769  nmfn0  29770  nmop0h  29774  nmcexi  29809  nmcopexi  29810  lnfn0i  29825  lnfnmuli  29827  nmcfnexi  29834  nlelshi  29843  riesz3i  29845  hmopidmchi  29934