Axiom ax-hvaddid 30951

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 30866	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c0v 30871	. . . 4 class 0ℎ
5		cva 30867	. . . 4 class +ℎ
6	1, 4, 5	co 7413	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1539	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30970  hvpncan  30986  hvsubeq0i  31010  hvsubcan2i  31011  hvsubaddi  31013  hvsub0  31023  hvaddsub4  31025  norm3difi  31094  shsel1  31268  shunssi  31315  omlsilem  31349  pjoc1i  31378  pjchi  31379  spansncvi  31599  5oalem1  31601  5oalem2  31602  3oalem2  31610  pjssmii  31628  hoaddridi  31733  lnop0  31913  lnopmul  31914  lnfn0i  31989  lnfnmuli  31991  pjclem4  32146  pj3si  32154  hst1h  32174  sumdmdlem  32365