Axiom ax-hv0cl 8794

Description: The zero vector is in the vector space.

Assertion

Ref	Expression
ax-hv0cl	|- 0h e. H~

Detailed syntax breakdown of Axiom ax-hv0cl

Step	Hyp	Ref	Expression
1		c0v 8730	. 2 class 0h
2		chil 8727	. 2 class H~
3	1, 2	wcel 955	1 wff 0h e. H~

This axiom is referenced by:  hvaddid2t 8813  hvmul0t 8814  hv2negt 8818  hvsubsub4t 8848  hvnegdit 8855  hvsubeq0t 8856  hvaddcant 8858  hvsub0t 8864  hvsubaddt 8865  hi01t 8883  hi02t 8884  normlem9at 8908  norm0 8916  normsqt 8922  normsub0t 8924  norm-iit 8926  norm-iiit 8928  normsubt 8931  normnegt 8932  normpytht 8933  norm3dif 8935  norm3dift 8938  norm3lemt 8940  norm3adift 8941  normpart 8943  polidt 8947  hilabl 8948  hilid 8949  bcst 8969  hlim0 9026  hlimcau 9028  hlimuni 9030  helch 9037  hsn0elch 9041  elch0 9047  hhssnv 9054  ocsh 9072  occllem2 9090  occllem8 9096  projlem8 9109  pjthlem13 9146  pjtht 9149  axpjpjt 9171  pjoc1t 9182  pjoc2t 9187  shscl 9196  choc0 9205  shintcl 9208  h1de2ct 9395  spansnt 9398  elspansnt 9405  elspansn2t 9406  h1datomt 9422  spansnjt 9509  spansncvt 9515  pjch1t 9532  pjadjt 9547  pjaddt 9548  pjinormt 9549  pjsubt 9550  pjmult 9551  pjcjt2 9554  pj0 9555  pjcht 9556  pjopytht 9582  pjnormt 9586  pjpytht 9587  pjnelt 9588  df0op2 9595  hon0 9636  ho01 9671  eigret 9678  eigortht 9681  nmopsetn0 9709  nmfnsetn0 9722  dmadjrnb 9747  nmopge0t 9751  nmfnge0t 9767  bra0 9790  lnop0t 9806  lnopmult 9807  0cnop 9819  nmop0 9826  nmfn0 9827  nmop0h 9831  lnopeq0lem2 9846  lnopuni 9852  lnophm 9858  nmcopexlem2 9867  lnfn0 9886  lnfnmul 9888  nmcfnexlem2 9896  nlelsh 9908  riesz3 9910  hmopidmch 9990  pjss2co 10003  pjssmt 10004  pjssge0t 10005  pjdifnormt 10006

Copyright terms: Public domain