Axiom ax-hvaddid 28437

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 28352	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c0v 28357	. . . 4 class 0ℎ
5		cva 28353	. . . 4 class +ℎ
6	1, 4, 5	co 6924	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1601	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  28456  hvpncan  28472  hvsubeq0i  28496  hvsubcan2i  28497  hvsubaddi  28499  hvsub0  28509  hvaddsub4  28511  norm3difi  28580  shsel1  28756  shunssi  28803  omlsilem  28837  pjoc1i  28866  pjchi  28867  spansncvi  29087  5oalem1  29089  5oalem2  29090  3oalem2  29098  pjssmii  29116  hoaddid1i  29221  lnop0  29401  lnopmul  29402  lnfn0i  29477  lnfnmuli  29479  pjclem4  29634  pj3si  29642  hst1h  29662  sumdmdlem  29853