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 31061
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 30982 . 2 class 0
2 chba 30977 . 2 class
31, 2wcel 2114 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  31080  hvaddlid  31081  hvmul0  31082  hv2neg  31086  hvsub0  31134  hi01  31154  hi02  31155  norm0  31186  normneg  31202  norm3difi  31205  hilablo  31218  hilid  31219  hlim0  31293  helch  31301  hsn0elch  31306  elch0  31312  hhssnv  31322  ocsh  31341  shscli  31375  choc0  31384  shintcli  31387  pj0i  31751  df0op2  31810  hon0  31851  ho01i  31886  nmopsetn0  31923  nmfnsetn0  31936  dmadjrnb  31964  nmopge0  31969  nmfnge0  31985  bra0  32008  lnop0  32024  lnopmul  32025  0cnop  32037  nmop0  32044  nmfn0  32045  nmop0h  32049  nmcexi  32084  nmcopexi  32085  lnfn0i  32100  lnfnmuli  32102  nmcfnexi  32109  nlelshi  32118  riesz3i  32120  hmopidmchi  32209
  Copyright terms: Public domain W3C validator