Axiom ax-hvaddid 31485

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 31400	. . 3 class ℋ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℋ
4		c0v 31405	. . . 4 class 0ℎ
5		cva 31401	. . . 4 class +ℎ
6	1, 4, 5	co 7413	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1570	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is used by:  hvaddlid  31504  hvpncan  31520  hvsubeq0i  31544  hvsubcan2i  31545  hvsubaddi  31547  hvsub0  31557  hvaddsub4  31559  norm3difi  31628  shsel1  31802  shunssi  31849  omlsilem  31883  pjoc1i  31912  pjchi  31913  spansncvi  32133  5oalem1  32135  5oalem2  32136  3oalem2  32144  pjssmii  32162  hoaddridi  32267  lnop0  32447  lnopmul  32448  lnfn0i  32523  lnfnmuli  32525  pjclem4  32680  pj3si  32688  hst1h  32708  sumdmdlem  32899