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 28194
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 chil 28109 . . 3 class
31, 2wcel 2145 . 2 wff 𝐴 ∈ ℋ
4 c0v 28114 . . . 4 class 0
5 cva 28110 . . . 4 class +
61, 4, 5co 6791 . . 3 class (𝐴 + 0)
76, 1wceq 1631 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddid2  28213  hvpncan  28229  hvsubeq0i  28253  hvsubcan2i  28254  hvsubaddi  28256  hvsub0  28266  hvaddsub4  28268  norm3difi  28337  shsel1  28513  shunssi  28560  omlsilem  28594  pjoc1i  28623  pjchi  28624  spansncvi  28844  5oalem1  28846  5oalem2  28847  3oalem2  28855  pjssmii  28873  hoaddid1i  28978  lnop0  29158  lnopmul  29159  lnfn0i  29234  lnfnmuli  29236  pjclem4  29391  pj3si  29399  hst1h  29419  sumdmdlem  29610
  Copyright terms: Public domain W3C validator