Axiom ax-hvaddid 30933

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 30848	. . 3 class ℋ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℋ
4		c0v 30853	. . . 4 class 0ℎ
5		cva 30849	. . . 4 class +ℎ
6	1, 4, 5	co 7387	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1540	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30952  hvpncan  30968  hvsubeq0i  30992  hvsubcan2i  30993  hvsubaddi  30995  hvsub0  31005  hvaddsub4  31007  norm3difi  31076  shsel1  31250  shunssi  31297  omlsilem  31331  pjoc1i  31360  pjchi  31361  spansncvi  31581  5oalem1  31583  5oalem2  31584  3oalem2  31592  pjssmii  31610  hoaddridi  31715  lnop0  31895  lnopmul  31896  lnfn0i  31971  lnfnmuli  31973  pjclem4  32128  pj3si  32136  hst1h  32156  sumdmdlem  32347