Axiom ax-hvaddid 27245

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		chil 27160	. . 3 class ℋ
3	1, 2	wcel 1977	. 2 wff 𝐴 ∈ ℋ
4		c0v 27165	. . . 4 class 0ℎ
5		cva 27161	. . . 4 class +ℎ
6	1, 4, 5	co 6549	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1475	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  27264  hvpncan  27280  hvsubeq0i  27304  hvsubcan2i  27305  hvsubaddi  27307  hvsub0  27317  hvaddsub4  27319  norm3difi  27388  shsel1  27564  shunssi  27611  omlsilem  27645  pjoc1i  27674  pjchi  27675  spansncvi  27895  5oalem1  27897  5oalem2  27898  3oalem2  27906  pjssmii  27924  hoaddid1i  28029  lnop0  28209  lnopmul  28210  lnfn0i  28285  lnfnmuli  28287  pjclem4  28442  pj3si  28450  hst1h  28470  sumdmdlem  28661