Axiom ax-hv0cl 31031

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 30952	. 2 class 0ℎ
2		chba 30947	. 2 class ℋ
3	1, 2	wcel 2105	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31050  hvaddlid  31051  hvmul0  31052  hv2neg  31056  hvsub0  31104  hi01  31124  hi02  31125  norm0  31156  normneg  31172  norm3difi  31175  hilablo  31188  hilid  31189  hlim0  31263  helch  31271  hsn0elch  31276  elch0  31282  hhssnv  31292  ocsh  31311  shscli  31345  choc0  31354  shintcli  31357  pj0i  31721  df0op2  31780  hon0  31821  ho01i  31856  nmopsetn0  31893  nmfnsetn0  31906  dmadjrnb  31934  nmopge0  31939  nmfnge0  31955  bra0  31978  lnop0  31994  lnopmul  31995  0cnop  32007  nmop0  32014  nmfn0  32015  nmop0h  32019  nmcexi  32054  nmcopexi  32055  lnfn0i  32070  lnfnmuli  32072  nmcfnexi  32079  nlelshi  32088  riesz3i  32090  hmopidmchi  32179