Axiom ax-hv0cl 29374

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 29295	. 2 class 0ℎ
2		chba 29290	. 2 class ℋ
3	1, 2	wcel 2107	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  29393  hvaddid2  29394  hvmul0  29395  hv2neg  29399  hvsub0  29447  hi01  29467  hi02  29468  norm0  29499  normneg  29515  norm3difi  29518  hilablo  29531  hilid  29532  hlim0  29606  helch  29614  hsn0elch  29619  elch0  29625  hhssnv  29635  ocsh  29654  shscli  29688  choc0  29697  shintcli  29700  pj0i  30064  df0op2  30123  hon0  30164  ho01i  30199  nmopsetn0  30236  nmfnsetn0  30249  dmadjrnb  30277  nmopge0  30282  nmfnge0  30298  bra0  30321  lnop0  30337  lnopmul  30338  0cnop  30350  nmop0  30357  nmfn0  30358  nmop0h  30362  nmcexi  30397  nmcopexi  30398  lnfn0i  30413  lnfnmuli  30415  nmcfnexi  30422  nlelshi  30431  riesz3i  30433  hmopidmchi  30522