Axiom ax-hvaddid 28433

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 28348	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c0v 28353	. . . 4 class 0ℎ
5		cva 28349	. . . 4 class +ℎ
6	1, 4, 5	co 6922	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1601	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  28452  hvpncan  28468  hvsubeq0i  28492  hvsubcan2i  28493  hvsubaddi  28495  hvsub0  28505  hvaddsub4  28507  norm3difi  28576  shsel1  28752  shunssi  28799  omlsilem  28833  pjoc1i  28862  pjchi  28863  spansncvi  29083  5oalem1  29085  5oalem2  29086  3oalem2  29094  pjssmii  29112  hoaddid1i  29217  lnop0  29397  lnopmul  29398  lnfn0i  29473  lnfnmuli  29475  pjclem4  29630  pj3si  29638  hst1h  29658  sumdmdlem  29849