Axiom ax-hvaddid 30940

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 30855	. . 3 class ℋ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℋ
4		c0v 30860	. . . 4 class 0ℎ
5		cva 30856	. . . 4 class +ℎ
6	1, 4, 5	co 7390	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1540	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30959  hvpncan  30975  hvsubeq0i  30999  hvsubcan2i  31000  hvsubaddi  31002  hvsub0  31012  hvaddsub4  31014  norm3difi  31083  shsel1  31257  shunssi  31304  omlsilem  31338  pjoc1i  31367  pjchi  31368  spansncvi  31588  5oalem1  31590  5oalem2  31591  3oalem2  31599  pjssmii  31617  hoaddridi  31722  lnop0  31902  lnopmul  31903  lnfn0i  31978  lnfnmuli  31980  pjclem4  32135  pj3si  32143  hst1h  32163  sumdmdlem  32354