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 28449
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 28370 . 2 class 0
2 chba 28365 . 2 class
31, 2wcel 2107 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  28468  hvaddid2  28469  hvmul0  28470  hv2neg  28474  hvsub0  28522  hi01  28542  hi02  28543  norm0  28574  normneg  28590  norm3difi  28593  hilablo  28606  hilid  28607  hlim0  28681  helch  28689  hsn0elch  28694  elch0  28700  hhssnv  28710  ocsh  28731  shscli  28765  choc0  28774  shintcli  28777  pj0i  29141  df0op2  29200  hon0  29241  ho01i  29276  nmopsetn0  29313  nmfnsetn0  29326  dmadjrnb  29354  nmopge0  29359  nmfnge0  29375  bra0  29398  lnop0  29414  lnopmul  29415  0cnop  29427  nmop0  29434  nmfn0  29435  nmop0h  29439  nmcexi  29474  nmcopexi  29475  lnfn0i  29490  lnfnmuli  29492  nmcfnexi  29499  nlelshi  29508  riesz3i  29510  hmopidmchi  29599
  Copyright terms: Public domain W3C validator