Axiom ax-hvaddid 28765

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 28680	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c0v 28685	. . . 4 class 0ℎ
5		cva 28681	. . . 4 class +ℎ
6	1, 4, 5	co 7142	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1537	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  28784  hvpncan  28800  hvsubeq0i  28824  hvsubcan2i  28825  hvsubaddi  28827  hvsub0  28837  hvaddsub4  28839  norm3difi  28908  shsel1  29082  shunssi  29129  omlsilem  29163  pjoc1i  29192  pjchi  29193  spansncvi  29413  5oalem1  29415  5oalem2  29416  3oalem2  29424  pjssmii  29442  hoaddid1i  29547  lnop0  29727  lnopmul  29728  lnfn0i  29803  lnfnmuli  29805  pjclem4  29960  pj3si  29968  hst1h  29988  sumdmdlem  30179