Axiom ax-hv0cl 8956

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 8874	. 2 class 0h
2		chil 8871	. 2 class H~
3	1, 2	wcel 999	1 wff 0h e. H~

This axiom is referenced by:  hvaddid2 8975  hvmul0 8976  hv2neg 8980  hvsubsub4 9010  hvnegdi 9017  hvsubeq0 9018  hvaddcan 9020  hvsub0 9026  hvsubadd 9027  hi01 9045  hi02 9046  normlem9at 9070  norm0 9078  normsq 9084  normsub0 9086  norm-ii 9088  norm-iii 9090  normsub 9093  normneg 9094  normpyth 9095  norm3difi 9097  norm3dif 9100  norm3lemt 9102  norm3adifi 9103  normpar 9105  polid 9109  hilabl 9110  hilid 9111  bcs 9131  hlim0 9188  hlimcaui 9190  hlimunii 9192  helch 9199  hsn0elch 9203  elch0 9209  hhssnv 9217  ocsh 9239  occllem2 9257  occllem8 9263  projlem8 9276  pjthlem13 9314  pjth 9317  axpjpj 9339  pjoc1 9350  pjoc2 9355  shscli 9364  choc0 9373  shintcli 9376  h1de2ci 9562  spansn 9565  elspansn 9572  elspansn2 9573  h1datom 9588  spansnj 9675  spansncv 9681  pjch1 9698  pjadji 9713  pjaddi 9714  pjinormi 9715  pjsubi 9716  pjmuli 9717  pjcjt2 9720  pj0i 9721  pjch 9722  pjopyth 9748  pjnorm 9752  pjpyth 9753  pjnel 9754  df0op2 9761  hon0 9802  ho01i 9837  eigre 9844  eigorth 9847  nmopsetn0 9875  nmfnsetn0 9888  dmadjrnb 9913  nmopge0 9918  nmfnge0 9934  bra0 9957  lnop0 9973  lnopmul 9974  0cnop 9986  nmop0 9993  nmfn0 9994  nmop0h 9999  lnopeq0lem2 10014  lnopunii 10020  lnophmi 10026  nmcopexlem2 10035  lnfn0i 10054  lnfnmuli 10056  nmcfnexlem2 10064  nlelshi 10076  riesz3i 10078  hmopidmchi 10162  pjss2coi 10175  pjssmi 10176  pjssge0i 10177  pjdifnormi 10178

Copyright terms: Public domain