Axiom ax-hvaddid 30245

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 30160	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c0v 30165	. . . 4 class 0ℎ
5		cva 30161	. . . 4 class +ℎ
6	1, 4, 5	co 7406	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1542	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30264  hvpncan  30280  hvsubeq0i  30304  hvsubcan2i  30305  hvsubaddi  30307  hvsub0  30317  hvaddsub4  30319  norm3difi  30388  shsel1  30562  shunssi  30609  omlsilem  30643  pjoc1i  30672  pjchi  30673  spansncvi  30893  5oalem1  30895  5oalem2  30896  3oalem2  30904  pjssmii  30922  hoaddridi  31027  lnop0  31207  lnopmul  31208  lnfn0i  31283  lnfnmuli  31285  pjclem4  31440  pj3si  31448  hst1h  31468  sumdmdlem  31659