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 27831
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 27746 . . 3 class
31, 2wcel 1988 . 2 wff 𝐴 ∈ ℋ
4 c0v 27751 . . . 4 class 0
5 cva 27747 . . . 4 class +
61, 4, 5co 6635 . . 3 class (𝐴 + 0)
76, 1wceq 1481 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddid2  27850  hvpncan  27866  hvsubeq0i  27890  hvsubcan2i  27891  hvsubaddi  27893  hvsub0  27903  hvaddsub4  27905  norm3difi  27974  shsel1  28150  shunssi  28197  omlsilem  28231  pjoc1i  28260  pjchi  28261  spansncvi  28481  5oalem1  28483  5oalem2  28484  3oalem2  28492  pjssmii  28510  hoaddid1i  28615  lnop0  28795  lnopmul  28796  lnfn0i  28871  lnfnmuli  28873  pjclem4  29028  pj3si  29036  hst1h  29056  sumdmdlem  29247
  Copyright terms: Public domain W3C validator