Axiom ax-hvaddid 27989

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		chil 27904	. . 3 class ℋ
3	1, 2	wcel 2030	. 2 wff 𝐴 ∈ ℋ
4		c0v 27909	. . . 4 class 0ℎ
5		cva 27905	. . . 4 class +ℎ
6	1, 4, 5	co 6690	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1523	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  28008  hvpncan  28024  hvsubeq0i  28048  hvsubcan2i  28049  hvsubaddi  28051  hvsub0  28061  hvaddsub4  28063  norm3difi  28132  shsel1  28308  shunssi  28355  omlsilem  28389  pjoc1i  28418  pjchi  28419  spansncvi  28639  5oalem1  28641  5oalem2  28642  3oalem2  28650  pjssmii  28668  hoaddid1i  28773  lnop0  28953  lnopmul  28954  lnfn0i  29029  lnfnmuli  29031  pjclem4  29186  pj3si  29194  hst1h  29214  sumdmdlem  29405