Axiom ax-hv0cl 31366

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 31287	. 2 class 0ℎ
2		chba 31282	. 2 class ℋ
3	1, 2	wcel 2142	1 wff 0ℎ ∈ ℋ

This axiom is used by:  ifhvhv0  31385  hvaddlid  31386  hvmul0  31387  hv2neg  31391  hvsub0  31439  hi01  31459  hi02  31460  norm0  31491  normneg  31507  norm3difi  31510  hilablo  31523  hilid  31524  hlim0  31598  helch  31606  hsn0elch  31611  elch0  31617  hhssnv  31627  ocsh  31646  shscli  31680  choc0  31689  shintcli  31692  pj0i  32056  df0op2  32115  hon0  32156  ho01i  32191  nmopsetn0  32228  nmfnsetn0  32241  dmadjrnb  32269  nmopge0  32274  nmfnge0  32290  bra0  32313  lnop0  32329  lnopmul  32330  0cnop  32342  nmop0  32349  nmfn0  32350  nmop0h  32354  nmcexi  32389  nmcopexi  32390  lnfn0i  32405  lnfnmuli  32407  nmcfnexi  32414  nlelshi  32423  riesz3i  32425  hmopidmchi  32514