Axiom ax-hv0cl 31605

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 31526	. 2 class 0ℎ
2		chba 31521	. 2 class ℋ
3	1, 2	wcel 2144	1 wff 0ℎ ∈ ℋ

This axiom is used by:  ifhvhv0  31624  hvaddlid  31625  hvmul0  31626  hv2neg  31630  hvsub0  31678  hi01  31698  hi02  31699  norm0  31730  normneg  31746  norm3difi  31749  hilablo  31762  hilid  31763  hlim0  31837  helch  31845  hsn0elch  31850  elch0  31856  hhssnv  31866  ocsh  31885  shscli  31919  choc0  31928  shintcli  31931  pj0i  32295  df0op2  32354  hon0  32395  ho01i  32430  nmopsetn0  32467  nmfnsetn0  32480  dmadjrnb  32508  nmopge0  32513  nmfnge0  32529  bra0  32552  lnop0  32568  lnopmul  32569  0cnop  32581  nmop0  32588  nmfn0  32589  nmop0h  32593  nmcexi  32628  nmcopexi  32629  lnfn0i  32644  lnfnmuli  32646  nmcfnexi  32653  nlelshi  32662  riesz3i  32664  hmopidmchi  32753