Axiom ax-hvaddid 31599

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 31514	. . 3 class ℋ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℋ
4		c0v 31519	. . . 4 class 0ℎ
5		cva 31515	. . . 4 class +ℎ
6	1, 4, 5	co 7418	. . 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  31618  hvpncan  31634  hvsubeq0i  31658  hvsubcan2i  31659  hvsubaddi  31661  hvsub0  31671  hvaddsub4  31673  norm3difi  31742  shsel1  31916  shunssi  31963  omlsilem  31997  pjoc1i  32026  pjchi  32027  spansncvi  32247  5oalem1  32249  5oalem2  32250  3oalem2  32258  pjssmii  32276  hoaddridi  32381  lnop0  32561  lnopmul  32562  lnfn0i  32637  lnfnmuli  32639  pjclem4  32794  pj3si  32802  hst1h  32822  sumdmdlem  33013