Axiom ax-hvaddid 31100

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 31015	. . 3 class ℋ
3	1, 2	wcel 2119	. 2 wff 𝐴 ∈ ℋ
4		c0v 31020	. . . 4 class 0ℎ
5		cva 31016	. . . 4 class +ℎ
6	1, 4, 5	co 7363	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1547	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31119  hvpncan  31135  hvsubeq0i  31159  hvsubcan2i  31160  hvsubaddi  31162  hvsub0  31172  hvaddsub4  31174  norm3difi  31243  shsel1  31417  shunssi  31464  omlsilem  31498  pjoc1i  31527  pjchi  31528  spansncvi  31748  5oalem1  31750  5oalem2  31751  3oalem2  31759  pjssmii  31777  hoaddridi  31882  lnop0  32062  lnopmul  32063  lnfn0i  32138  lnfnmuli  32140  pjclem4  32295  pj3si  32303  hst1h  32323  sumdmdlem  32514