Axiom ax-hv0cl 31083

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 31004	. 2 class 0ℎ
2		chba 30999	. 2 class ℋ
3	1, 2	wcel 2114	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31102  hvaddlid  31103  hvmul0  31104  hv2neg  31108  hvsub0  31156  hi01  31176  hi02  31177  norm0  31208  normneg  31224  norm3difi  31227  hilablo  31240  hilid  31241  hlim0  31315  helch  31323  hsn0elch  31328  elch0  31334  hhssnv  31344  ocsh  31363  shscli  31397  choc0  31406  shintcli  31409  pj0i  31773  df0op2  31832  hon0  31873  ho01i  31908  nmopsetn0  31945  nmfnsetn0  31958  dmadjrnb  31986  nmopge0  31991  nmfnge0  32007  bra0  32030  lnop0  32046  lnopmul  32047  0cnop  32059  nmop0  32066  nmfn0  32067  nmop0h  32071  nmcexi  32106  nmcopexi  32107  lnfn0i  32122  lnfnmuli  32124  nmcfnexi  32131  nlelshi  32140  riesz3i  32142  hmopidmchi  32231