HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hvaddid Structured version   Visualization version   GIF version

Axiom ax-hvaddid 28762
Description: Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hvaddid (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)

Detailed syntax breakdown of Axiom ax-hvaddid
StepHypRef Expression
1 cA . . 3 class 𝐴
2 chba 28677 . . 3 class
31, 2wcel 2114 . 2 wff 𝐴 ∈ ℋ
4 c0v 28682 . . . 4 class 0
5 cva 28678 . . . 4 class +
61, 4, 5co 7129 . . 3 class (𝐴 + 0)
76, 1wceq 1537 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddid2  28781  hvpncan  28797  hvsubeq0i  28821  hvsubcan2i  28822  hvsubaddi  28824  hvsub0  28834  hvaddsub4  28836  norm3difi  28905  shsel1  29079  shunssi  29126  omlsilem  29160  pjoc1i  29189  pjchi  29190  spansncvi  29410  5oalem1  29412  5oalem2  29413  3oalem2  29421  pjssmii  29439  hoaddid1i  29544  lnop0  29724  lnopmul  29725  lnfn0i  29800  lnfnmuli  29802  pjclem4  29957  pj3si  29965  hst1h  29985  sumdmdlem  30176
  Copyright terms: Public domain W3C validator