HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hv0cl Structured version   Visualization version   GIF version

Axiom ax-hv0cl 27988
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
StepHypRef Expression
1 c0v 27909 . 2 class 0
2 chil 27904 . 2 class
31, 2wcel 2030 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  28007  hvaddid2  28008  hvmul0  28009  hv2neg  28013  hvsub0  28061  hi01  28081  hi02  28082  norm0  28113  normneg  28129  norm3difi  28132  hilablo  28145  hilid  28146  hlim0  28220  helch  28228  hsn0elch  28233  elch0  28239  hhssnv  28249  ocsh  28270  shscli  28304  choc0  28313  shintcli  28316  pj0i  28680  df0op2  28739  hon0  28780  ho01i  28815  nmopsetn0  28852  nmfnsetn0  28865  dmadjrnb  28893  nmopge0  28898  nmfnge0  28914  bra0  28937  lnop0  28953  lnopmul  28954  0cnop  28966  nmop0  28973  nmfn0  28974  nmop0h  28978  nmcexi  29013  nmcopexi  29014  lnfn0i  29029  lnfnmuli  29031  nmcfnexi  29038  nlelshi  29047  riesz3i  29049  hmopidmchi  29138
  Copyright terms: Public domain W3C validator