Axiom ax-hvaddid 31079

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 30994	. . 3 class ℋ
3	1, 2	wcel 2113	. 2 wff 𝐴 ∈ ℋ
4		c0v 30999	. . . 4 class 0ℎ
5		cva 30995	. . . 4 class +ℎ
6	1, 4, 5	co 7358	. . 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  31098  hvpncan  31114  hvsubeq0i  31138  hvsubcan2i  31139  hvsubaddi  31141  hvsub0  31151  hvaddsub4  31153  norm3difi  31222  shsel1  31396  shunssi  31443  omlsilem  31477  pjoc1i  31506  pjchi  31507  spansncvi  31727  5oalem1  31729  5oalem2  31730  3oalem2  31738  pjssmii  31756  hoaddridi  31861  lnop0  32041  lnopmul  32042  lnfn0i  32117  lnfnmuli  32119  pjclem4  32274  pj3si  32282  hst1h  32302  sumdmdlem  32493