Axiom ax-hvaddid 30966

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 30881	. . 3 class ℋ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℋ
4		c0v 30886	. . . 4 class 0ℎ
5		cva 30882	. . . 4 class +ℎ
6	1, 4, 5	co 7353	. . 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  30985  hvpncan  31001  hvsubeq0i  31025  hvsubcan2i  31026  hvsubaddi  31028  hvsub0  31038  hvaddsub4  31040  norm3difi  31109  shsel1  31283  shunssi  31330  omlsilem  31364  pjoc1i  31393  pjchi  31394  spansncvi  31614  5oalem1  31616  5oalem2  31617  3oalem2  31625  pjssmii  31643  hoaddridi  31748  lnop0  31928  lnopmul  31929  lnfn0i  32004  lnfnmuli  32006  pjclem4  32161  pj3si  32169  hst1h  32189  sumdmdlem  32380