Axiom ax-hv0cl 31470

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 31391	. 2 class 0ℎ
2		chba 31386	. 2 class ℋ
3	1, 2	wcel 2145	1 wff 0ℎ ∈ ℋ

This axiom is used by:  ifhvhv0  31489  hvaddlid  31490  hvmul0  31491  hv2neg  31495  hvsub0  31543  hi01  31563  hi02  31564  norm0  31595  normneg  31611  norm3difi  31614  hilablo  31627  hilid  31628  hlim0  31702  helch  31710  hsn0elch  31715  elch0  31721  hhssnv  31731  ocsh  31750  shscli  31784  choc0  31793  shintcli  31796  pj0i  32160  df0op2  32219  hon0  32260  ho01i  32295  nmopsetn0  32332  nmfnsetn0  32345  dmadjrnb  32373  nmopge0  32378  nmfnge0  32394  bra0  32417  lnop0  32433  lnopmul  32434  0cnop  32446  nmop0  32453  nmfn0  32454  nmop0h  32458  nmcexi  32493  nmcopexi  32494  lnfn0i  32509  lnfnmuli  32511  nmcfnexi  32518  nlelshi  32527  riesz3i  32529  hmopidmchi  32618