Axiom ax-hvaddid 31036

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 30951	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c0v 30956	. . . 4 class 0ℎ
5		cva 30952	. . . 4 class +ℎ
6	1, 4, 5	co 7448	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1537	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31055  hvpncan  31071  hvsubeq0i  31095  hvsubcan2i  31096  hvsubaddi  31098  hvsub0  31108  hvaddsub4  31110  norm3difi  31179  shsel1  31353  shunssi  31400  omlsilem  31434  pjoc1i  31463  pjchi  31464  spansncvi  31684  5oalem1  31686  5oalem2  31687  3oalem2  31695  pjssmii  31713  hoaddridi  31818  lnop0  31998  lnopmul  31999  lnfn0i  32074  lnfnmuli  32076  pjclem4  32231  pj3si  32239  hst1h  32259  sumdmdlem  32450