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 28437
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 28352 . . 3 class
31, 2wcel 2107 . 2 wff 𝐴 ∈ ℋ
4 c0v 28357 . . . 4 class 0
5 cva 28353 . . . 4 class +
61, 4, 5co 6924 . . 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  28456  hvpncan  28472  hvsubeq0i  28496  hvsubcan2i  28497  hvsubaddi  28499  hvsub0  28509  hvaddsub4  28511  norm3difi  28580  shsel1  28756  shunssi  28803  omlsilem  28837  pjoc1i  28866  pjchi  28867  spansncvi  29087  5oalem1  29089  5oalem2  29090  3oalem2  29098  pjssmii  29116  hoaddid1i  29221  lnop0  29401  lnopmul  29402  lnfn0i  29477  lnfnmuli  29479  pjclem4  29634  pj3si  29642  hst1h  29662  sumdmdlem  29853
  Copyright terms: Public domain W3C validator