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 27026
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 26947 . 2 class 0
2 chil 26942 . 2 class
31, 2wcel 1938 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  27045  hvaddid2  27046  hvmul0  27047  hv2neg  27051  hvsub0  27099  hi01  27119  hi02  27120  norm0  27151  normneg  27167  norm3difi  27170  hilablo  27183  hilid  27184  hlim0  27258  helch  27266  hsn0elch  27271  elch0  27277  hhssnv  27287  ocsh  27308  shscli  27342  choc0  27351  shintcli  27354  pj0i  27718  df0op2  27777  hon0  27818  ho01i  27853  nmopsetn0  27890  nmfnsetn0  27903  dmadjrnb  27931  nmopge0  27936  nmfnge0  27952  bra0  27975  lnop0  27991  lnopmul  27992  0cnop  28004  nmop0  28011  nmfn0  28012  nmop0h  28016  nmcexi  28051  nmcopexi  28052  lnfn0i  28067  lnfnmuli  28069  nmcfnexi  28076  nlelshi  28085  riesz3i  28087  hmopidmchi  28176
  Copyright terms: Public domain W3C validator