Axiom ax-hvaddid 30525

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 30440	. . 3 class ℋ
3	1, 2	wcel 2105	. 2 wff 𝐴 ∈ ℋ
4		c0v 30445	. . . 4 class 0ℎ
5		cva 30441	. . . 4 class +ℎ
6	1, 4, 5	co 7412	. . 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  30544  hvpncan  30560  hvsubeq0i  30584  hvsubcan2i  30585  hvsubaddi  30587  hvsub0  30597  hvaddsub4  30599  norm3difi  30668  shsel1  30842  shunssi  30889  omlsilem  30923  pjoc1i  30952  pjchi  30953  spansncvi  31173  5oalem1  31175  5oalem2  31176  3oalem2  31184  pjssmii  31202  hoaddridi  31307  lnop0  31487  lnopmul  31488  lnfn0i  31563  lnfnmuli  31565  pjclem4  31720  pj3si  31728  hst1h  31748  sumdmdlem  31939