Axiom ax-hv0cl 10297

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 10215	. 2 class 0h
2		chil 10212	. 2 class ~H
3	1, 2	wcel 1138	1 wff 0h e. ~H

This axiom is referenced by:  hvaddid2 10316  hvmul0 10317  hv2neg 10321  hvsubsub4 10351  hvnegdi 10358  hvsubeq0 10359  hvaddcan 10361  hvsub0 10368  hvsubadd 10369  hi01 10387  hi02 10388  normlem9at 10412  norm0 10420  normsq 10426  normsub0 10428  norm-ii 10430  norm-iii 10432  normsub 10435  normneg 10436  normpyth 10437  norm3difi 10439  norm3dif 10442  norm3lemt 10444  norm3adifi 10445  normpar 10447  polid 10451  hilabl 10452  hilid 10453  bcs 10473  hlim0 10530  hlimcaui 10532  hlimunii 10534  helch 10541  hsn0elch 10545  elch0 10551  hhssnv 10559  ocsh 10581  occllem2 10599  occllem8 10605  projlem8 10618  pjthlem13 10656  pjth 10659  axpjpj 10681  pjoc1 10692  pjoc2 10697  shscli 10706  choc0 10715  shintcli 10718  h1de2ci 10904  spansn 10907  elspansn 10914  elspansn2 10915  h1datom 10930  spansnj 11019  spansncv 11025  pjch1 11042  pjadji 11057  pjaddi 11058  pjinormi 11059  pjsubi 11060  pjmuli 11061  pjcjt2 11064  pj0i 11065  pjch 11066  pjopyth 11092  pjnorm 11096  pjpyth 11097  pjnel 11098  df0op2 11107  hon0 11148  ho01i 11183  eigre 11190  eigorth 11193  nmopsetn0 11221  nmfnsetn0 11234  dmadjrnb 11259  nmopge0 11264  nmfnge0 11280  bra0 11303  lnop0 11319  lnopmul 11320  0cnop 11332  nmop0 11339  nmfn0 11340  nmop0h 11345  lnopeq0lem2 11360  lnopunii 11366  lnophmi 11372  nmcopexlem2 11381  lnfn0i 11400  lnfnmuli 11402  nmcfnexlem2 11410  nlelshi 11422  riesz3i 11424  hmopidmchi 11515  pjss2coi 11528  pjssmi 11529  pjssge0i 11530  pjdifnormi 11531

Copyright terms: Public domain