Axiom ax-hvaddid 8829

Description: Addition with the zero vector.

Assertion

Ref	Expression
ax-hvaddid	⊢ (A ∈ ℋ → (A +h 0h) = A)

Detailed syntax breakdown of Axiom ax-hvaddid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 8743	. . 3 class ℋ
3	1, 2	wcel 957	. 2 wff A ∈ ℋ
4		c0v 8746	. . . 4 class 0h
5		cva 8744	. . . 4 class +h
6	1, 4, 5	co 3958	. . 3 class (A +h 0h)
7	6, 1	wceq 955	. 2 wff (A +h 0h) = A
8	3, 7	wi 3	1 wff (A ∈ ℋ → (A +h 0h) = A)

This axiom is referenced by:  hvaddid2t 8847  hvpncant 8863  hvsubeq0 8885  hvsubcan2 8886  hvsubadd 8888  hvsub0t 8898  hvaddsub4t 8900  norm3dif 8969  chocuni 9127  pjthlem14 9187  omlsilem 9199  pjoc1 9219  pjch 9220  shsel1t 9240  shunss 9292  spansncv 9554  5oalem1 9556  5oalem2 9557  3oalem2 9565  pjssm 9583  pjv 9607  hoaddid1 9669  lnop0t 9847  lnopmult 9848  lnfn0 9927  lnfnmul 9929  pjclem4 10083  pj3s 10091  hst1ht 10110  sumdmdlem 10301

Copyright terms: Public domain