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 27027
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 26942 . . 3 class
31, 2wcel 1938 . 2 wff 𝐴 ∈ ℋ
4 c0v 26947 . . . 4 class 0
5 cva 26943 . . . 4 class +
61, 4, 5co 6431 . . 3 class (𝐴 + 0)
76, 1wceq 1474 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddid2  27046  hvpncan  27062  hvsubeq0i  27086  hvsubcan2i  27087  hvsubaddi  27089  hvsub0  27099  hvaddsub4  27101  norm3difi  27170  shsel1  27346  shunssi  27393  omlsilem  27427  pjoc1i  27456  pjchi  27457  spansncvi  27677  5oalem1  27679  5oalem2  27680  3oalem2  27688  pjssmii  27706  hoaddid1i  27811  lnop0  27991  lnopmul  27992  lnfn0i  28067  lnfnmuli  28069  pjclem4  28224  pj3si  28232  hst1h  28252  sumdmdlem  28443
  Copyright terms: Public domain W3C validator