Axiom ax-hvaddid 31337

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 31252	. . 3 class ℋ
3	1, 2	wcel 2143	. 2 wff 𝐴 ∈ ℋ
4		c0v 31257	. . . 4 class 0ℎ
5		cva 31253	. . . 4 class +ℎ
6	1, 4, 5	co 7412	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1570	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31356  hvpncan  31372  hvsubeq0i  31396  hvsubcan2i  31397  hvsubaddi  31399  hvsub0  31409  hvaddsub4  31411  norm3difi  31480  shsel1  31654  shunssi  31701  omlsilem  31735  pjoc1i  31764  pjchi  31765  spansncvi  31985  5oalem1  31987  5oalem2  31988  3oalem2  31996  pjssmii  32014  hoaddridi  32119  lnop0  32299  lnopmul  32300  lnfn0i  32375  lnfnmuli  32377  pjclem4  32532  pj3si  32540  hst1h  32560  sumdmdlem  32751