Axiom ax-hvaddid 30931

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 30846	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c0v 30851	. . . 4 class 0ℎ
5		cva 30847	. . . 4 class +ℎ
6	1, 4, 5	co 7403	. . 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  30950  hvpncan  30966  hvsubeq0i  30990  hvsubcan2i  30991  hvsubaddi  30993  hvsub0  31003  hvaddsub4  31005  norm3difi  31074  shsel1  31248  shunssi  31295  omlsilem  31329  pjoc1i  31358  pjchi  31359  spansncvi  31579  5oalem1  31581  5oalem2  31582  3oalem2  31590  pjssmii  31608  hoaddridi  31713  lnop0  31893  lnopmul  31894  lnfn0i  31969  lnfnmuli  31971  pjclem4  32126  pj3si  32134  hst1h  32154  sumdmdlem  32345