Axiom ax-hv0cl 30939

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 30860	. 2 class 0ℎ
2		chba 30855	. 2 class ℋ
3	1, 2	wcel 2109	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  30958  hvaddlid  30959  hvmul0  30960  hv2neg  30964  hvsub0  31012  hi01  31032  hi02  31033  norm0  31064  normneg  31080  norm3difi  31083  hilablo  31096  hilid  31097  hlim0  31171  helch  31179  hsn0elch  31184  elch0  31190  hhssnv  31200  ocsh  31219  shscli  31253  choc0  31262  shintcli  31265  pj0i  31629  df0op2  31688  hon0  31729  ho01i  31764  nmopsetn0  31801  nmfnsetn0  31814  dmadjrnb  31842  nmopge0  31847  nmfnge0  31863  bra0  31886  lnop0  31902  lnopmul  31903  0cnop  31915  nmop0  31922  nmfn0  31923  nmop0h  31927  nmcexi  31962  nmcopexi  31963  lnfn0i  31978  lnfnmuli  31980  nmcfnexi  31987  nlelshi  31996  riesz3i  31998  hmopidmchi  32087