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 30886
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 30801 . . 3 class
31, 2wcel 2098 . 2 wff 𝐴 ∈ ℋ
4 c0v 30806 . . . 4 class 0
5 cva 30802 . . . 4 class +
61, 4, 5co 7419 . . 3 class (𝐴 + 0)
76, 1wceq 1533 . 2 wff (𝐴 + 0) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℋ → (𝐴 + 0) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  hvaddlid  30905  hvpncan  30921  hvsubeq0i  30945  hvsubcan2i  30946  hvsubaddi  30948  hvsub0  30958  hvaddsub4  30960  norm3difi  31029  shsel1  31203  shunssi  31250  omlsilem  31284  pjoc1i  31313  pjchi  31314  spansncvi  31534  5oalem1  31536  5oalem2  31537  3oalem2  31545  pjssmii  31563  hoaddridi  31668  lnop0  31848  lnopmul  31849  lnfn0i  31924  lnfnmuli  31926  pjclem4  32081  pj3si  32089  hst1h  32109  sumdmdlem  32300
  Copyright terms: Public domain W3C validator