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 28200
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 28121 . 2 class 0
2 chil 28116 . 2 class
31, 2wcel 2145 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  28219  hvaddid2  28220  hvmul0  28221  hv2neg  28225  hvsub0  28273  hi01  28293  hi02  28294  norm0  28325  normneg  28341  norm3difi  28344  hilablo  28357  hilid  28358  hlim0  28432  helch  28440  hsn0elch  28445  elch0  28451  hhssnv  28461  ocsh  28482  shscli  28516  choc0  28525  shintcli  28528  pj0i  28892  df0op2  28951  hon0  28992  ho01i  29027  nmopsetn0  29064  nmfnsetn0  29077  dmadjrnb  29105  nmopge0  29110  nmfnge0  29126  bra0  29149  lnop0  29165  lnopmul  29166  0cnop  29178  nmop0  29185  nmfn0  29186  nmop0h  29190  nmcexi  29225  nmcopexi  29226  lnfn0i  29241  lnfnmuli  29243  nmcfnexi  29250  nlelshi  29259  riesz3i  29261  hmopidmchi  29350
  Copyright terms: Public domain W3C validator