Axiom ax-hvaddid 28787

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 28702	. . 3 class ℋ
3	1, 2	wcel 2111	. 2 wff 𝐴 ∈ ℋ
4		c0v 28707	. . . 4 class 0ℎ
5		cva 28703	. . . 4 class +ℎ
6	1, 4, 5	co 7135	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1538	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  28806  hvpncan  28822  hvsubeq0i  28846  hvsubcan2i  28847  hvsubaddi  28849  hvsub0  28859  hvaddsub4  28861  norm3difi  28930  shsel1  29104  shunssi  29151  omlsilem  29185  pjoc1i  29214  pjchi  29215  spansncvi  29435  5oalem1  29437  5oalem2  29438  3oalem2  29446  pjssmii  29464  hoaddid1i  29569  lnop0  29749  lnopmul  29750  lnfn0i  29825  lnfnmuli  29827  pjclem4  29982  pj3si  29990  hst1h  30010  sumdmdlem  30201