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 31023
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 30938 . . 3 class
31, 2wcel 2108 . 2 wff 𝐴 ∈ ℋ
4 c0v 30943 . . . 4 class 0
5 cva 30939 . . . 4 class +
61, 4, 5co 7431 . . 3 class (𝐴 + 0)
76, 1wceq 1540 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddlid  31042  hvpncan  31058  hvsubeq0i  31082  hvsubcan2i  31083  hvsubaddi  31085  hvsub0  31095  hvaddsub4  31097  norm3difi  31166  shsel1  31340  shunssi  31387  omlsilem  31421  pjoc1i  31450  pjchi  31451  spansncvi  31671  5oalem1  31673  5oalem2  31674  3oalem2  31682  pjssmii  31700  hoaddridi  31805  lnop0  31985  lnopmul  31986  lnfn0i  32061  lnfnmuli  32063  pjclem4  32218  pj3si  32226  hst1h  32246  sumdmdlem  32437
  Copyright terms: Public domain W3C validator