Axiom ax-hvaddid 8957

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 8871	. . 3 class H~
3	1, 2	wcel 999	. 2 wff A e. H~
4		c0v 8874	. . . 4 class 0h
5		cva 8872	. . . 4 class +h
6	1, 4, 5	co 4021	. . 3 class (A +h 0h)
7	6, 1	wceq 997	. 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 8975  hvpncan 8991  hvsubeq0i 9013  hvsubcan2i 9014  hvsubaddi 9016  hvsub0 9026  hvaddsub4 9028  norm3difi 9097  chocunii 9255  pjthlem14 9315  omlsilem 9327  pjoc1i 9347  pjchi 9348  shsel1 9368  shunssi 9420  spansncvi 9680  5oalem1 9682  5oalem2 9683  3oalem2 9691  pjssmii 9709  pjvi 9733  hoaddid1i 9795  lnop0 9973  lnopmul 9974  lnfn0i 10054  lnfnmuli 10056  pjclem4 10211  pj3si 10219  hst1h 10238  sumdmdlem 10429

Copyright terms: Public domain