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 31321
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 31242 . 2 class 0
2 chba 31237 . 2 class
31, 2wcel 2141 1 wff 0 ∈ ℋ
Colors of variables: wff setvar class
This axiom is referenced by:  ifhvhv0  31340  hvaddlid  31341  hvmul0  31342  hv2neg  31346  hvsub0  31394  hi01  31414  hi02  31415  norm0  31446  normneg  31462  norm3difi  31465  hilablo  31478  hilid  31479  hlim0  31553  helch  31561  hsn0elch  31566  elch0  31572  hhssnv  31582  ocsh  31601  shscli  31635  choc0  31644  shintcli  31647  pj0i  32011  df0op2  32070  hon0  32111  ho01i  32146  nmopsetn0  32183  nmfnsetn0  32196  dmadjrnb  32224  nmopge0  32229  nmfnge0  32245  bra0  32268  lnop0  32284  lnopmul  32285  0cnop  32297  nmop0  32304  nmfn0  32305  nmop0h  32309  nmcexi  32344  nmcopexi  32345  lnfn0i  32360  lnfnmuli  32362  nmcfnexi  32369  nlelshi  32378  riesz3i  32380  hmopidmchi  32469
  Copyright terms: Public domain W3C validator