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 27830
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 27751 . 2 class 0
2 chil 27746 . 2 class
31, 2wcel 1988 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  27849  hvaddid2  27850  hvmul0  27851  hv2neg  27855  hvsub0  27903  hi01  27923  hi02  27924  norm0  27955  normneg  27971  norm3difi  27974  hilablo  27987  hilid  27988  hlim0  28062  helch  28070  hsn0elch  28075  elch0  28081  hhssnv  28091  ocsh  28112  shscli  28146  choc0  28155  shintcli  28158  pj0i  28522  df0op2  28581  hon0  28622  ho01i  28657  nmopsetn0  28694  nmfnsetn0  28707  dmadjrnb  28735  nmopge0  28740  nmfnge0  28756  bra0  28779  lnop0  28795  lnopmul  28796  0cnop  28808  nmop0  28815  nmfn0  28816  nmop0h  28820  nmcexi  28855  nmcopexi  28856  lnfn0i  28871  lnfnmuli  28873  nmcfnexi  28880  nlelshi  28889  riesz3i  28891  hmopidmchi  28980
  Copyright terms: Public domain W3C validator