Axiom ax-hvaddid 28194

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 28109	. . 3 class ℋ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℋ
4		c0v 28114	. . . 4 class 0ℎ
5		cva 28110	. . . 4 class +ℎ
6	1, 4, 5	co 6791	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1631	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  28213  hvpncan  28229  hvsubeq0i  28253  hvsubcan2i  28254  hvsubaddi  28256  hvsub0  28266  hvaddsub4  28268  norm3difi  28337  shsel1  28513  shunssi  28560  omlsilem  28594  pjoc1i  28623  pjchi  28624  spansncvi  28844  5oalem1  28846  5oalem2  28847  3oalem2  28855  pjssmii  28873  hoaddid1i  28978  lnop0  29158  lnopmul  29159  lnfn0i  29234  lnfnmuli  29236  pjclem4  29391  pj3si  29399  hst1h  29419  sumdmdlem  29610