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 31296
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 31217 . 2 class 0
2 chba 31212 . 2 class
31, 2wcel 2149 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  31315  hvaddlid  31316  hvmul0  31317  hv2neg  31321  hvsub0  31369  hi01  31389  hi02  31390  norm0  31421  normneg  31437  norm3difi  31440  hilablo  31453  hilid  31454  hlim0  31528  helch  31536  hsn0elch  31541  elch0  31547  hhssnv  31557  ocsh  31576  shscli  31610  choc0  31619  shintcli  31622  pj0i  31986  df0op2  32045  hon0  32086  ho01i  32121  nmopsetn0  32158  nmfnsetn0  32171  dmadjrnb  32199  nmopge0  32204  nmfnge0  32220  bra0  32243  lnop0  32259  lnopmul  32260  0cnop  32272  nmop0  32279  nmfn0  32280  nmop0h  32284  nmcexi  32319  nmcopexi  32320  lnfn0i  32335  lnfnmuli  32337  nmcfnexi  32344  nlelshi  32353  riesz3i  32355  hmopidmchi  32444
  Copyright terms: Public domain W3C validator