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 27989
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 27904 . . 3 class
31, 2wcel 2030 . 2 wff 𝐴 ∈ ℋ
4 c0v 27909 . . . 4 class 0
5 cva 27905 . . . 4 class +
61, 4, 5co 6690 . . 3 class (𝐴 + 0)
76, 1wceq 1523 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddid2  28008  hvpncan  28024  hvsubeq0i  28048  hvsubcan2i  28049  hvsubaddi  28051  hvsub0  28061  hvaddsub4  28063  norm3difi  28132  shsel1  28308  shunssi  28355  omlsilem  28389  pjoc1i  28418  pjchi  28419  spansncvi  28639  5oalem1  28641  5oalem2  28642  3oalem2  28650  pjssmii  28668  hoaddid1i  28773  lnop0  28953  lnopmul  28954  lnfn0i  29029  lnfnmuli  29031  pjclem4  29186  pj3si  29194  hst1h  29214  sumdmdlem  29405
  Copyright terms: Public domain W3C validator