Axiom ax-hv0cl 28886

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 28807	. 2 class 0ℎ
2		chba 28802	. 2 class ℋ
3	1, 2	wcel 2112	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  28905  hvaddid2  28906  hvmul0  28907  hv2neg  28911  hvsub0  28959  hi01  28979  hi02  28980  norm0  29011  normneg  29027  norm3difi  29030  hilablo  29043  hilid  29044  hlim0  29118  helch  29126  hsn0elch  29131  elch0  29137  hhssnv  29147  ocsh  29166  shscli  29200  choc0  29209  shintcli  29212  pj0i  29576  df0op2  29635  hon0  29676  ho01i  29711  nmopsetn0  29748  nmfnsetn0  29761  dmadjrnb  29789  nmopge0  29794  nmfnge0  29810  bra0  29833  lnop0  29849  lnopmul  29850  0cnop  29862  nmop0  29869  nmfn0  29870  nmop0h  29874  nmcexi  29909  nmcopexi  29910  lnfn0i  29925  lnfnmuli  29927  nmcfnexi  29934  nlelshi  29943  riesz3i  29945  hmopidmchi  30034