Axiom ax-hv0cl 31062

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

This axiom is referenced by:  ifhvhv0  31081  hvaddlid  31082  hvmul0  31083  hv2neg  31087  hvsub0  31135  hi01  31155  hi02  31156  norm0  31187  normneg  31203  norm3difi  31206  hilablo  31219  hilid  31220  hlim0  31294  helch  31302  hsn0elch  31307  elch0  31313  hhssnv  31323  ocsh  31342  shscli  31376  choc0  31385  shintcli  31388  pj0i  31752  df0op2  31811  hon0  31852  ho01i  31887  nmopsetn0  31924  nmfnsetn0  31937  dmadjrnb  31965  nmopge0  31970  nmfnge0  31986  bra0  32009  lnop0  32025  lnopmul  32026  0cnop  32038  nmop0  32045  nmfn0  32046  nmop0h  32050  nmcexi  32085  nmcopexi  32086  lnfn0i  32101  lnfnmuli  32103  nmcfnexi  32110  nlelshi  32119  riesz3i  32121  hmopidmchi  32210