Axiom ax-hvaddid 8859

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 8773	. . 3 class H~
3	1, 2	wcel 958	. 2 wff A e. H~
4		c0v 8776	. . . 4 class 0h
5		cva 8774	. . . 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 8877  hvpncant 8893  hvsubeq0 8915  hvsubcan2 8916  hvsubadd 8918  hvsub0t 8928  hvaddsub4t 8930  norm3dif 8999  chocuni 9157  pjthlem14 9217  omlsilem 9229  pjoc1 9249  pjch 9250  shsel1t 9270  shunss 9322  spansncv 9582  5oalem1 9584  5oalem2 9585  3oalem2 9593  pjssm 9611  pjv 9635  hoaddid1 9697  lnop0t 9875  lnopmult 9876  lnfn0 9956  lnfnmul 9958  pjclem4 10112  pj3s 10120  hst1ht 10139  sumdmdlem 10330

Copyright terms: Public domain