Axiom ax-hvaddid 31075

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 30990	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c0v 30995	. . . 4 class 0ℎ
5		cva 30991	. . . 4 class +ℎ
6	1, 4, 5	co 7367	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1542	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31094  hvpncan  31110  hvsubeq0i  31134  hvsubcan2i  31135  hvsubaddi  31137  hvsub0  31147  hvaddsub4  31149  norm3difi  31218  shsel1  31392  shunssi  31439  omlsilem  31473  pjoc1i  31502  pjchi  31503  spansncvi  31723  5oalem1  31725  5oalem2  31726  3oalem2  31734  pjssmii  31752  hoaddridi  31857  lnop0  32037  lnopmul  32038  lnfn0i  32113  lnfnmuli  32115  pjclem4  32270  pj3si  32278  hst1h  32298  sumdmdlem  32489