Axiom ax-hvaddid 9149

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 9063	. . 3 class H~
3	1, 2	wcel 994	. 2 wff A e. H~
4		c0v 9066	. . . 4 class 0h
5		cva 9064	. . . 4 class +h
6	1, 4, 5	co 4021	. . 3 class (A +h 0h)
7	6, 1	wceq 992	. 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:  hvaddid2 9167  hvpncan 9183  hvsubeq0i 9205  hvsubcan2i 9206  hvsubaddi 9208  hvsub0 9219  hvaddsub4 9221  norm3difi 9290  chocunii 9448  pjthlem14 9508  omlsilem 9520  pjoc1i 9540  pjchi 9541  shsel1 9561  shunssi 9613  spansncvi 9875  5oalem1 9877  5oalem2 9878  3oalem2 9886  pjssmii 9904  pjvi 9928  hoaddid1i 9992  lnop0 10169  lnopmul 10170  lnfn0i 10250  lnfnmuli 10252  pjclem4 10408  pj3si 10416  hst1h 10435  sumdmdlem 10627

Copyright terms: Public domain