Axiom ax-hvaddid 31663

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 31578	. . 3 class ℋ
3	1, 2	wcel 2147	. 2 wff 𝐴 ∈ ℋ
4		c0v 31583	. . . 4 class 0ℎ
5		cva 31579	. . . 4 class +ℎ
6	1, 4, 5	co 7451	. . 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  31682  hvpncan  31698  hvsubeq0i  31722  hvsubcan2i  31723  hvsubaddi  31725  hvsub0  31735  hvaddsub4  31737  norm3difi  31806  shsel1  31980  shunssi  32027  omlsilem  32061  pjoc1i  32090  pjchi  32091  spansncvi  32311  5oalem1  32313  5oalem2  32314  3oalem2  32322  pjssmii  32340  hoaddridi  32445  lnop0  32625  lnopmul  32626  lnfn0i  32701  lnfnmuli  32703  pjclem4  32858  pj3si  32866  hst1h  32886  sumdmdlem  33077