Axiom ax-hvaddid 29267

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 29182	. . 3 class ℋ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℋ
4		c0v 29187	. . . 4 class 0ℎ
5		cva 29183	. . . 4 class +ℎ
6	1, 4, 5	co 7255	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1539	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  29286  hvpncan  29302  hvsubeq0i  29326  hvsubcan2i  29327  hvsubaddi  29329  hvsub0  29339  hvaddsub4  29341  norm3difi  29410  shsel1  29584  shunssi  29631  omlsilem  29665  pjoc1i  29694  pjchi  29695  spansncvi  29915  5oalem1  29917  5oalem2  29918  3oalem2  29926  pjssmii  29944  hoaddid1i  30049  lnop0  30229  lnopmul  30230  lnfn0i  30305  lnfnmuli  30307  pjclem4  30462  pj3si  30470  hst1h  30490  sumdmdlem  30681