Axiom ax-hvaddid 9022

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 8968	. . 3 class H~
3	1, 2	wcel 1105	. 2 wff A e. H~
4		c0v 8971	. . . 4 class 0h
5		cva 8969	. . . 4 class +h
6	1, 4, 5	co 3902	. . 3 class (A +h 0h)
7	6, 1	wceq 1099	. 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 9041  hvpncant 9057  hvsubeq0 9079  hvsubcan2 9080  hvsubadd 9082  hvsub0t 9092  hvaddsub4t 9094  norm3dif 9163  chocuni 9302  pjthlem14 9361  omlsilem 9373  pjoc1 9393  pjch 9394  shsel1t 9414  shunss 9466  spansncv 9728  5oalem1 9730  5oalem2 9731  3oalem2 9739  pjssm 9757  pjv 9781  hoaddid1 9843  lnop0t 10020  lnopmult 10021  lnfn0 10100  lnfnmul 10102  pjclem4 10251  pj3s 10259  hst1ht 10278  sumdmdlem 10466

Copyright terms: Public domain