Axiom ax-hv0cl 31074

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

This axiom is referenced by:  ifhvhv0  31093  hvaddlid  31094  hvmul0  31095  hv2neg  31099  hvsub0  31147  hi01  31167  hi02  31168  norm0  31199  normneg  31215  norm3difi  31218  hilablo  31231  hilid  31232  hlim0  31306  helch  31314  hsn0elch  31319  elch0  31325  hhssnv  31335  ocsh  31354  shscli  31388  choc0  31397  shintcli  31400  pj0i  31764  df0op2  31823  hon0  31864  ho01i  31899  nmopsetn0  31936  nmfnsetn0  31949  dmadjrnb  31977  nmopge0  31982  nmfnge0  31998  bra0  32021  lnop0  32037  lnopmul  32038  0cnop  32050  nmop0  32057  nmfn0  32058  nmop0h  32062  nmcexi  32097  nmcopexi  32098  lnfn0i  32113  lnfnmuli  32115  nmcfnexi  32122  nlelshi  32131  riesz3i  32133  hmopidmchi  32222