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 28433
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 28348 . . 3 class
31, 2wcel 2107 . 2 wff 𝐴 ∈ ℋ
4 c0v 28353 . . . 4 class 0
5 cva 28349 . . . 4 class +
61, 4, 5co 6922 . . 3 class (𝐴 + 0)
76, 1wceq 1601 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddid2  28452  hvpncan  28468  hvsubeq0i  28492  hvsubcan2i  28493  hvsubaddi  28495  hvsub0  28505  hvaddsub4  28507  norm3difi  28576  shsel1  28752  shunssi  28799  omlsilem  28833  pjoc1i  28862  pjchi  28863  spansncvi  29083  5oalem1  29085  5oalem2  29086  3oalem2  29094  pjssmii  29112  hoaddid1i  29217  lnop0  29397  lnopmul  29398  lnfn0i  29473  lnfnmuli  29475  pjclem4  29630  pj3si  29638  hst1h  29658  sumdmdlem  29849
  Copyright terms: Public domain W3C validator