Axiom ax-hv0cl 31321

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 31242	. 2 class 0ℎ
2		chba 31237	. 2 class ℋ
3	1, 2	wcel 2141	1 wff 0ℎ ∈ ℋ

This axiom is referenced by:  ifhvhv0  31340  hvaddlid  31341  hvmul0  31342  hv2neg  31346  hvsub0  31394  hi01  31414  hi02  31415  norm0  31446  normneg  31462  norm3difi  31465  hilablo  31478  hilid  31479  hlim0  31553  helch  31561  hsn0elch  31566  elch0  31572  hhssnv  31582  ocsh  31601  shscli  31635  choc0  31644  shintcli  31647  pj0i  32011  df0op2  32070  hon0  32111  ho01i  32146  nmopsetn0  32183  nmfnsetn0  32196  dmadjrnb  32224  nmopge0  32229  nmfnge0  32245  bra0  32268  lnop0  32284  lnopmul  32285  0cnop  32297  nmop0  32304  nmfn0  32305  nmop0h  32309  nmcexi  32344  nmcopexi  32345  lnfn0i  32360  lnfnmuli  32362  nmcfnexi  32369  nlelshi  32378  riesz3i  32380  hmopidmchi  32469