Axiom ax-hvaddid 8795

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 8727	. . 3 class ℋ
3	1, 2	wcel 955	. 2 wff A ∈ ℋ
4		c0v 8730	. . . 4 class 0h
5		cva 8728	. . . 4 class +h
6	1, 4, 5	co 3948	. . 3 class (A +h 0h)
7	6, 1	wceq 953	. 2 wff (A +h 0h) = A
8	3, 7	wi 3	1 wff (A ∈ ℋ → (A +h 0h) = A)

This axiom is referenced by:  hvaddid2t 8813  hvpncant 8829  hvsubeq0 8851  hvsubcan2 8852  hvsubadd 8854  hvsub0t 8864  hvaddsub4t 8866  norm3dif 8935  chocuni 9088  pjthlem14 9147  omlsilem 9159  pjoc1 9179  pjch 9180  shsel1t 9200  shunss 9252  spansncv 9514  5oalem1 9516  5oalem2 9517  3oalem2 9525  pjssm 9543  pjv 9567  hoaddid1 9629  lnop0t 9806  lnopmult 9807  lnfn0 9886  lnfnmul 9888  pjclem4 10037  pj3s 10045  hst1ht 10064  sumdmdlem 10252

Copyright terms: Public domain