Axiom ax-hvaddid 31293

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 31208	. . 3 class ℋ
3	1, 2	wcel 2149	. 2 wff 𝐴 ∈ ℋ
4		c0v 31213	. . . 4 class 0ℎ
5		cva 31209	. . . 4 class +ℎ
6	1, 4, 5	co 7408	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1567	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31312  hvpncan  31328  hvsubeq0i  31352  hvsubcan2i  31353  hvsubaddi  31355  hvsub0  31365  hvaddsub4  31367  norm3difi  31436  shsel1  31610  shunssi  31657  omlsilem  31691  pjoc1i  31720  pjchi  31721  spansncvi  31941  5oalem1  31943  5oalem2  31944  3oalem2  31952  pjssmii  31970  hoaddridi  32075  lnop0  32255  lnopmul  32256  lnfn0i  32331  lnfnmuli  32333  pjclem4  32488  pj3si  32496  hst1h  32516  sumdmdlem  32707