Axiom ax-hvaddid 31090

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 31005	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c0v 31010	. . . 4 class 0ℎ
5		cva 31006	. . . 4 class +ℎ
6	1, 4, 5	co 7360	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1542	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31109  hvpncan  31125  hvsubeq0i  31149  hvsubcan2i  31150  hvsubaddi  31152  hvsub0  31162  hvaddsub4  31164  norm3difi  31233  shsel1  31407  shunssi  31454  omlsilem  31488  pjoc1i  31517  pjchi  31518  spansncvi  31738  5oalem1  31740  5oalem2  31741  3oalem2  31749  pjssmii  31767  hoaddridi  31872  lnop0  32052  lnopmul  32053  lnfn0i  32128  lnfnmuli  32130  pjclem4  32285  pj3si  32293  hst1h  32313  sumdmdlem  32504