Axiom ax-hvaddid 30986

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 30901	. . 3 class ℋ
3	1, 2	wcel 2113	. 2 wff 𝐴 ∈ ℋ
4		c0v 30906	. . . 4 class 0ℎ
5		cva 30902	. . . 4 class +ℎ
6	1, 4, 5	co 7352	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1541	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31005  hvpncan  31021  hvsubeq0i  31045  hvsubcan2i  31046  hvsubaddi  31048  hvsub0  31058  hvaddsub4  31060  norm3difi  31129  shsel1  31303  shunssi  31350  omlsilem  31384  pjoc1i  31413  pjchi  31414  spansncvi  31634  5oalem1  31636  5oalem2  31637  3oalem2  31645  pjssmii  31663  hoaddridi  31768  lnop0  31948  lnopmul  31949  lnfn0i  32024  lnfnmuli  32026  pjclem4  32181  pj3si  32189  hst1h  32209  sumdmdlem  32400