Axiom ax-hvaddid 27861

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		chil 27776	. . 3 class ℋ
3	1, 2	wcel 1990	. 2 wff 𝐴 ∈ ℋ
4		c0v 27781	. . . 4 class 0ℎ
5		cva 27777	. . . 4 class +ℎ
6	1, 4, 5	co 6650	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1483	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  27880  hvpncan  27896  hvsubeq0i  27920  hvsubcan2i  27921  hvsubaddi  27923  hvsub0  27933  hvaddsub4  27935  norm3difi  28004  shsel1  28180  shunssi  28227  omlsilem  28261  pjoc1i  28290  pjchi  28291  spansncvi  28511  5oalem1  28513  5oalem2  28514  3oalem2  28522  pjssmii  28540  hoaddid1i  28645  lnop0  28825  lnopmul  28826  lnfn0i  28901  lnfnmuli  28903  pjclem4  29058  pj3si  29066  hst1h  29086  sumdmdlem  29277