Axiom ax-hvaddid 31612

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 31527	. . 3 class ℋ
3	1, 2	wcel 2144	. 2 wff 𝐴 ∈ ℋ
4		c0v 31532	. . . 4 class 0ℎ
5		cva 31528	. . . 4 class +ℎ
6	1, 4, 5	co 7421	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1569	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is used by:  hvaddlid  31631  hvpncan  31647  hvsubeq0i  31671  hvsubcan2i  31672  hvsubaddi  31674  hvsub0  31684  hvaddsub4  31686  norm3difi  31755  shsel1  31929  shunssi  31976  omlsilem  32010  pjoc1i  32039  pjchi  32040  spansncvi  32260  5oalem1  32262  5oalem2  32263  3oalem2  32271  pjssmii  32289  hoaddridi  32394  lnop0  32574  lnopmul  32575  lnfn0i  32650  lnfnmuli  32652  pjclem4  32807  pj3si  32815  hst1h  32835  sumdmdlem  33026