Axiom ax-hvaddid 8874

Description: Addition with the zero vector.

Assertion

Ref	Expression
ax-hvaddid	|- (A e. H~ -> (A +h 0h) = A)

Detailed syntax breakdown of Axiom ax-hvaddid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 8788	. . 3 class H~
3	1, 2	wcel 958	. 2 wff A e. H~
4		c0v 8791	. . . 4 class 0h
5		cva 8789	. . . 4 class +h
6	1, 4, 5	co 3963	. . 3 class (A +h 0h)
7	6, 1	wceq 956	. 2 wff (A +h 0h) = A
8	3, 7	wi 3	1 wff (A e. H~ -> (A +h 0h) = A)

This axiom is referenced by:  hvaddid2t 8892  hvpncant 8908  hvsubeq0 8930  hvsubcan2 8931  hvsubadd 8933  hvsub0t 8943  hvaddsub4t 8945  norm3dif 9014  chocuni 9172  pjthlem14 9232  omlsilem 9244  pjoc1 9264  pjch 9265  shsel1t 9285  shunss 9337  spansncv 9597  5oalem1 9599  5oalem2 9600  3oalem2 9608  pjssm 9626  pjv 9650  hoaddid1 9712  lnop0t 9890  lnopmult 9891  lnfn0 9971  lnfnmul 9973  pjclem4 10127  pj3s 10135  hst1ht 10154  sumdmdlem 10345

Copyright terms: Public domain