Axiom ax-hv0cl 31035

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

This axiom is referenced by:  ifhvhv0  31054  hvaddlid  31055  hvmul0  31056  hv2neg  31060  hvsub0  31108  hi01  31128  hi02  31129  norm0  31160  normneg  31176  norm3difi  31179  hilablo  31192  hilid  31193  hlim0  31267  helch  31275  hsn0elch  31280  elch0  31286  hhssnv  31296  ocsh  31315  shscli  31349  choc0  31358  shintcli  31361  pj0i  31725  df0op2  31784  hon0  31825  ho01i  31860  nmopsetn0  31897  nmfnsetn0  31910  dmadjrnb  31938  nmopge0  31943  nmfnge0  31959  bra0  31982  lnop0  31998  lnopmul  31999  0cnop  32011  nmop0  32018  nmfn0  32019  nmop0h  32023  nmcexi  32058  nmcopexi  32059  lnfn0i  32074  lnfnmuli  32076  nmcfnexi  32083  nlelshi  32092  riesz3i  32094  hmopidmchi  32183