Axiom ax-hvaddid 31023

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		chba 30938	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c0v 30943	. . . 4 class 0ℎ
5		cva 30939	. . . 4 class +ℎ
6	1, 4, 5	co 7431	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1540	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31042  hvpncan  31058  hvsubeq0i  31082  hvsubcan2i  31083  hvsubaddi  31085  hvsub0  31095  hvaddsub4  31097  norm3difi  31166  shsel1  31340  shunssi  31387  omlsilem  31421  pjoc1i  31450  pjchi  31451  spansncvi  31671  5oalem1  31673  5oalem2  31674  3oalem2  31682  pjssmii  31700  hoaddridi  31805  lnop0  31985  lnopmul  31986  lnfn0i  32061  lnfnmuli  32063  pjclem4  32218  pj3si  32226  hst1h  32246  sumdmdlem  32437