Axiom ax-hvaddid 28781

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 28696	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c0v 28701	. . . 4 class 0ℎ
5		cva 28697	. . . 4 class +ℎ
6	1, 4, 5	co 7156	. . 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  28800  hvpncan  28816  hvsubeq0i  28840  hvsubcan2i  28841  hvsubaddi  28843  hvsub0  28853  hvaddsub4  28855  norm3difi  28924  shsel1  29098  shunssi  29145  omlsilem  29179  pjoc1i  29208  pjchi  29209  spansncvi  29429  5oalem1  29431  5oalem2  29432  3oalem2  29440  pjssmii  29458  hoaddid1i  29563  lnop0  29743  lnopmul  29744  lnfn0i  29819  lnfnmuli  29821  pjclem4  29976  pj3si  29984  hst1h  30004  sumdmdlem  30195