Axiom ax-hvaddid 30979

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 30894	. . 3 class ℋ
3	1, 2	wcel 2111	. 2 wff 𝐴 ∈ ℋ
4		c0v 30899	. . . 4 class 0ℎ
5		cva 30895	. . . 4 class +ℎ
6	1, 4, 5	co 7346	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1541	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30998  hvpncan  31014  hvsubeq0i  31038  hvsubcan2i  31039  hvsubaddi  31041  hvsub0  31051  hvaddsub4  31053  norm3difi  31122  shsel1  31296  shunssi  31343  omlsilem  31377  pjoc1i  31406  pjchi  31407  spansncvi  31627  5oalem1  31629  5oalem2  31630  3oalem2  31638  pjssmii  31656  hoaddridi  31761  lnop0  31941  lnopmul  31942  lnfn0i  32017  lnfnmuli  32019  pjclem4  32174  pj3si  32182  hst1h  32202  sumdmdlem  32393