Axiom ax-hvaddid 31091

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 31006	. . 3 class ℋ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℋ
4		c0v 31011	. . . 4 class 0ℎ
5		cva 31007	. . . 4 class +ℎ
6	1, 4, 5	co 7368	. . 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  31110  hvpncan  31126  hvsubeq0i  31150  hvsubcan2i  31151  hvsubaddi  31153  hvsub0  31163  hvaddsub4  31165  norm3difi  31234  shsel1  31408  shunssi  31455  omlsilem  31489  pjoc1i  31518  pjchi  31519  spansncvi  31739  5oalem1  31741  5oalem2  31742  3oalem2  31750  pjssmii  31768  hoaddridi  31873  lnop0  32053  lnopmul  32054  lnfn0i  32129  lnfnmuli  32131  pjclem4  32286  pj3si  32294  hst1h  32314  sumdmdlem  32505