Axiom ax-hv0cl 30965

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

This axiom is referenced by:  ifhvhv0  30984  hvaddlid  30985  hvmul0  30986  hv2neg  30990  hvsub0  31038  hi01  31058  hi02  31059  norm0  31090  normneg  31106  norm3difi  31109  hilablo  31122  hilid  31123  hlim0  31197  helch  31205  hsn0elch  31210  elch0  31216  hhssnv  31226  ocsh  31245  shscli  31279  choc0  31288  shintcli  31291  pj0i  31655  df0op2  31714  hon0  31755  ho01i  31790  nmopsetn0  31827  nmfnsetn0  31840  dmadjrnb  31868  nmopge0  31873  nmfnge0  31889  bra0  31912  lnop0  31928  lnopmul  31929  0cnop  31941  nmop0  31948  nmfn0  31949  nmop0h  31953  nmcexi  31988  nmcopexi  31989  lnfn0i  32004  lnfnmuli  32006  nmcfnexi  32013  nlelshi  32022  riesz3i  32024  hmopidmchi  32113