Axiom ax-hvaddid 31385

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 31300	. . 3 class ℋ
3	1, 2	wcel 2146	. 2 wff 𝐴 ∈ ℋ
4		c0v 31305	. . . 4 class 0ℎ
5		cva 31301	. . . 4 class +ℎ
6	1, 4, 5	co 7416	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1570	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is used by:  hvaddlid  31404  hvpncan  31420  hvsubeq0i  31444  hvsubcan2i  31445  hvsubaddi  31447  hvsub0  31457  hvaddsub4  31459  norm3difi  31528  shsel1  31702  shunssi  31749  omlsilem  31783  pjoc1i  31812  pjchi  31813  spansncvi  32033  5oalem1  32035  5oalem2  32036  3oalem2  32044  pjssmii  32062  hoaddridi  32167  lnop0  32347  lnopmul  32348  lnfn0i  32423  lnfnmuli  32425  pjclem4  32580  pj3si  32588  hst1h  32608  sumdmdlem  32799