Axiom ax-hv0cl 31141

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 31062	. 2 class 0ℎ
2		chba 31057	. 2 class ℋ
3	1, 2	wcel 2132	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31160  hvaddlid  31161  hvmul0  31162  hv2neg  31166  hvsub0  31214  hi01  31234  hi02  31235  norm0  31266  normneg  31282  norm3difi  31285  hilablo  31298  hilid  31299  hlim0  31373  helch  31381  hsn0elch  31386  elch0  31392  hhssnv  31402  ocsh  31421  shscli  31455  choc0  31464  shintcli  31467  pj0i  31831  df0op2  31890  hon0  31931  ho01i  31966  nmopsetn0  32003  nmfnsetn0  32016  dmadjrnb  32044  nmopge0  32049  nmfnge0  32065  bra0  32088  lnop0  32104  lnopmul  32105  0cnop  32117  nmop0  32124  nmfn0  32125  nmop0h  32129  nmcexi  32164  nmcopexi  32165  lnfn0i  32180  lnfnmuli  32182  nmcfnexi  32189  nlelshi  32198  riesz3i  32200  hmopidmchi  32289