Axiom ax-hvaddid 31032

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 30947	. . 3 class ℋ
3	1, 2	wcel 2105	. 2 wff 𝐴 ∈ ℋ
4		c0v 30952	. . . 4 class 0ℎ
5		cva 30948	. . . 4 class +ℎ
6	1, 4, 5	co 7430	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1536	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31051  hvpncan  31067  hvsubeq0i  31091  hvsubcan2i  31092  hvsubaddi  31094  hvsub0  31104  hvaddsub4  31106  norm3difi  31175  shsel1  31349  shunssi  31396  omlsilem  31430  pjoc1i  31459  pjchi  31460  spansncvi  31680  5oalem1  31682  5oalem2  31683  3oalem2  31691  pjssmii  31709  hoaddridi  31814  lnop0  31994  lnopmul  31995  lnfn0i  32070  lnfnmuli  32072  pjclem4  32227  pj3si  32235  hst1h  32255  sumdmdlem  32446