Axiom ax-hvaddid 30295

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 30210	. . 3 class ℋ
3	1, 2	wcel 2106	. 2 wff 𝐴 ∈ ℋ
4		c0v 30215	. . . 4 class 0ℎ
5		cva 30211	. . . 4 class +ℎ
6	1, 4, 5	co 7411	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1541	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30314  hvpncan  30330  hvsubeq0i  30354  hvsubcan2i  30355  hvsubaddi  30357  hvsub0  30367  hvaddsub4  30369  norm3difi  30438  shsel1  30612  shunssi  30659  omlsilem  30693  pjoc1i  30722  pjchi  30723  spansncvi  30943  5oalem1  30945  5oalem2  30946  3oalem2  30954  pjssmii  30972  hoaddridi  31077  lnop0  31257  lnopmul  31258  lnfn0i  31333  lnfnmuli  31335  pjclem4  31490  pj3si  31498  hst1h  31518  sumdmdlem  31709